Proof of Theorem infxpenc2lem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | infxpenc2.1 | . . 3
⊢ (𝜑 → 𝐴 ∈ On) | 
| 2 | 1 | mptexd 7245 | . 2
⊢ (𝜑 → (𝑏 ∈ 𝐴 ↦ 𝐺) ∈ V) | 
| 3 | 1 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐴 ∈ On) | 
| 4 |  | simprl 770 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝑏 ∈ 𝐴) | 
| 5 |  | onelon 6408 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ On) | 
| 6 | 3, 4, 5 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝑏 ∈ On) | 
| 7 |  | simprr 772 | . . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → ω ⊆ 𝑏) | 
| 8 |  | infxpenc2.2 | . . . . . . . 8
⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) | 
| 9 |  | infxpenc2.3 | . . . . . . . 8
⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑥))‘ran (𝑛‘𝑏)) | 
| 10 | 1, 8, 9 | infxpenc2lem1 10060 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝑊 ∈ (On ∖ 1o) ∧
(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊))) | 
| 11 | 10 | simpld 494 | . . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝑊 ∈ (On ∖
1o)) | 
| 12 |  | infxpenc2.4 | . . . . . . 7
⊢ (𝜑 → 𝐹:(ω ↑o
2o)–1-1-onto→ω) | 
| 13 | 12 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐹:(ω ↑o
2o)–1-1-onto→ω) | 
| 14 |  | infxpenc2.5 | . . . . . . 7
⊢ (𝜑 → (𝐹‘∅) = ∅) | 
| 15 | 14 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝐹‘∅) = ∅) | 
| 16 | 10 | simprd 495 | . . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊)) | 
| 17 |  | infxpenc2.k | . . . . . 6
⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑o
2o) ↑m 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) | 
| 18 |  | infxpenc2.h | . . . . . 6
⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑o 2o)
CNF 𝑊)) | 
| 19 |  | infxpenc2.l | . . . . . 6
⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑m (𝑊 ·o
2o)) ∣ 𝑥
finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦 ∘ ◡(𝑌 ∘ ◡𝑋)))) | 
| 20 |  | infxpenc2.x | . . . . . 6
⊢ 𝑋 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·o 𝑧) +o 𝑤)) | 
| 21 |  | infxpenc2.y | . . . . . 6
⊢ 𝑌 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((2o
·o 𝑤)
+o 𝑧)) | 
| 22 |  | infxpenc2.j | . . . . . 6
⊢ 𝐽 = (((ω CNF (2o
·o 𝑊))
∘ 𝐿) ∘ ◡(ω CNF (𝑊 ·o
2o))) | 
| 23 |  | infxpenc2.z | . . . . . 6
⊢ 𝑍 = (𝑥 ∈ (ω ↑o 𝑊), 𝑦 ∈ (ω ↑o 𝑊) ↦ (((ω
↑o 𝑊)
·o 𝑥)
+o 𝑦)) | 
| 24 |  | infxpenc2.t | . . . . . 6
⊢ 𝑇 = (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ 〈((𝑛‘𝑏)‘𝑥), ((𝑛‘𝑏)‘𝑦)〉) | 
| 25 |  | infxpenc2.g | . . . . . 6
⊢ 𝐺 = (◡(𝑛‘𝑏) ∘ (((𝐻 ∘ 𝐽) ∘ 𝑍) ∘ 𝑇)) | 
| 26 | 6, 7, 11, 13, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25 | infxpenc 10059 | . . . . 5
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏) | 
| 27 |  | f1of 6847 | . . . . . . . . 9
⊢ (𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏 → 𝐺:(𝑏 × 𝑏)⟶𝑏) | 
| 28 | 26, 27 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐺:(𝑏 × 𝑏)⟶𝑏) | 
| 29 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑏 ∈ V | 
| 30 | 29, 29 | xpex 7774 | . . . . . . . 8
⊢ (𝑏 × 𝑏) ∈ V | 
| 31 |  | fex 7247 | . . . . . . . 8
⊢ ((𝐺:(𝑏 × 𝑏)⟶𝑏 ∧ (𝑏 × 𝑏) ∈ V) → 𝐺 ∈ V) | 
| 32 | 28, 30, 31 | sylancl 586 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐺 ∈ V) | 
| 33 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑏 ∈ 𝐴 ↦ 𝐺) = (𝑏 ∈ 𝐴 ↦ 𝐺) | 
| 34 | 33 | fvmpt2 7026 | . . . . . . 7
⊢ ((𝑏 ∈ 𝐴 ∧ 𝐺 ∈ V) → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏) = 𝐺) | 
| 35 | 4, 32, 34 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏) = 𝐺) | 
| 36 | 35 | f1oeq1d 6842 | . . . . 5
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ 𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏)) | 
| 37 | 26, 36 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) | 
| 38 | 37 | expr 456 | . . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) | 
| 39 | 38 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) | 
| 40 |  | nfmpt1 5249 | . . . 4
⊢
Ⅎ𝑏(𝑏 ∈ 𝐴 ↦ 𝐺) | 
| 41 | 40 | nfeq2 2922 | . . 3
⊢
Ⅎ𝑏 𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) | 
| 42 |  | fveq1 6904 | . . . . 5
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → (𝑔‘𝑏) = ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏)) | 
| 43 | 42 | f1oeq1d 6842 | . . . 4
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → ((𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) | 
| 44 | 43 | imbi2d 340 | . . 3
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → ((ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) | 
| 45 | 41, 44 | ralbid 3272 | . 2
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → (∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) | 
| 46 | 2, 39, 45 | spcedv 3597 | 1
⊢ (𝜑 → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |