Proof of Theorem infxpenc2lem2
Step | Hyp | Ref
| Expression |
1 | | infxpenc2.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ On) |
2 | | mptexg 6389 |
. . 3
⊢ (𝐴 ∈ On → (𝑏 ∈ 𝐴 ↦ 𝐺) ∈ V) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (𝑏 ∈ 𝐴 ↦ 𝐺) ∈ V) |
4 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐴 ∈ On) |
5 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝑏 ∈ 𝐴) |
6 | | onelon 5665 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ On) |
7 | 4, 5, 6 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝑏 ∈ On) |
8 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → ω ⊆ 𝑏) |
9 | | infxpenc2.2 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
10 | | infxpenc2.3 |
. . . . . . . 8
⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))‘ran (𝑛‘𝑏)) |
11 | 1, 9, 10 | infxpenc2lem1 8725 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝑊 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊))) |
12 | 11 | simpld 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝑊 ∈ (On ∖
1𝑜)) |
13 | | infxpenc2.4 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(ω ↑𝑜
2𝑜)–1-1-onto→ω) |
14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐹:(ω ↑𝑜
2𝑜)–1-1-onto→ω) |
15 | | infxpenc2.5 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘∅) = ∅) |
16 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝐹‘∅) = ∅) |
17 | 11 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊)) |
18 | | infxpenc2.k |
. . . . . 6
⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑𝑜
2𝑜) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) |
19 | | infxpenc2.h |
. . . . . 6
⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑𝑜
2𝑜) CNF 𝑊)) |
20 | | infxpenc2.l |
. . . . . 6
⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚
(𝑊
·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾
ω) ∘ (𝑦 ∘
◡(𝑌 ∘ ◡𝑋)))) |
21 | | infxpenc2.x |
. . . . . 6
⊢ 𝑋 = (𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤)) |
22 | | infxpenc2.y |
. . . . . 6
⊢ 𝑌 = (𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((2𝑜
·𝑜 𝑤) +𝑜 𝑧)) |
23 | | infxpenc2.j |
. . . . . 6
⊢ 𝐽 = (((ω CNF
(2𝑜 ·𝑜 𝑊)) ∘ 𝐿) ∘ ◡(ω CNF (𝑊 ·𝑜
2𝑜))) |
24 | | infxpenc2.z |
. . . . . 6
⊢ 𝑍 = (𝑥 ∈ (ω ↑𝑜
𝑊), 𝑦 ∈ (ω ↑𝑜
𝑊) ↦ (((ω
↑𝑜 𝑊) ·𝑜 𝑥) +𝑜 𝑦)) |
25 | | infxpenc2.t |
. . . . . 6
⊢ 𝑇 = (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ 〈((𝑛‘𝑏)‘𝑥), ((𝑛‘𝑏)‘𝑦)〉) |
26 | | infxpenc2.g |
. . . . . 6
⊢ 𝐺 = (◡(𝑛‘𝑏) ∘ (((𝐻 ∘ 𝐽) ∘ 𝑍) ∘ 𝑇)) |
27 | 7, 8, 12, 14, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26 | infxpenc 8724 |
. . . . 5
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏) |
28 | | f1of 6050 |
. . . . . . . . 9
⊢ (𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏 → 𝐺:(𝑏 × 𝑏)⟶𝑏) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐺:(𝑏 × 𝑏)⟶𝑏) |
30 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
31 | 30, 30 | xpex 6860 |
. . . . . . . 8
⊢ (𝑏 × 𝑏) ∈ V |
32 | | fex 6394 |
. . . . . . . 8
⊢ ((𝐺:(𝑏 × 𝑏)⟶𝑏 ∧ (𝑏 × 𝑏) ∈ V) → 𝐺 ∈ V) |
33 | 29, 31, 32 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐺 ∈ V) |
34 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐴 ↦ 𝐺) = (𝑏 ∈ 𝐴 ↦ 𝐺) |
35 | 34 | fvmpt2 6200 |
. . . . . . 7
⊢ ((𝑏 ∈ 𝐴 ∧ 𝐺 ∈ V) → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏) = 𝐺) |
36 | 5, 33, 35 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏) = 𝐺) |
37 | | f1oeq1 6040 |
. . . . . 6
⊢ (((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏) = 𝐺 → (((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ 𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏)) |
38 | 36, 37 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ 𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏)) |
39 | 27, 38 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) |
40 | 39 | expr 641 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
41 | 40 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
42 | | nfmpt1 4675 |
. . . . 5
⊢
Ⅎ𝑏(𝑏 ∈ 𝐴 ↦ 𝐺) |
43 | 42 | nfeq2 2766 |
. . . 4
⊢
Ⅎ𝑏 𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) |
44 | | fveq1 6102 |
. . . . . 6
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → (𝑔‘𝑏) = ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏)) |
45 | | f1oeq1 6040 |
. . . . . 6
⊢ ((𝑔‘𝑏) = ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏) → ((𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
46 | 44, 45 | syl 17 |
. . . . 5
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → ((𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
47 | 46 | imbi2d 329 |
. . . 4
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → ((ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
48 | 43, 47 | ralbid 2966 |
. . 3
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → (∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
49 | 48 | spcegv 3267 |
. 2
⊢ ((𝑏 ∈ 𝐴 ↦ 𝐺) ∈ V → (∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
50 | 3, 41, 49 | sylc 63 |
1
⊢ (𝜑 → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |