Proof of Theorem cnfcom2lem
| Step | Hyp | Ref
| Expression |
| 1 | | cnfcom2.1 |
. . . . . 6
⊢ (𝜑 → ∅ ∈ 𝐵) |
| 2 | | n0i 4340 |
. . . . . 6
⊢ (∅
∈ 𝐵 → ¬ 𝐵 = ∅) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → ¬ 𝐵 = ∅) |
| 4 | | cnfcom.f |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) |
| 5 | | cnfcom.s |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 = dom (ω CNF 𝐴) |
| 6 | | omelon 9686 |
. . . . . . . . . . . . . . . . . 18
⊢ ω
∈ On |
| 7 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ω ∈
On) |
| 8 | | cnfcom.a |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ On) |
| 9 | 5, 7, 8 | cantnff1o 9736 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴)) |
| 10 | | f1ocnv 6860 |
. . . . . . . . . . . . . . . 16
⊢ ((ω
CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆) |
| 11 | | f1of 6848 |
. . . . . . . . . . . . . . . 16
⊢ (◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆) |
| 12 | 9, 10, 11 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆) |
| 13 | | cnfcom.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴)) |
| 14 | 12, 13 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆) |
| 15 | 4, 14 | eqeltrid 2845 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
| 16 | 5, 7, 8 | cantnfs 9706 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))) |
| 17 | 15, 16 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)) |
| 18 | 17 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶ω) |
| 19 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹:𝐴⟶ω) |
| 20 | 19 | feqmptd 6977 |
. . . . . . . . 9
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
| 21 | | dif0 4378 |
. . . . . . . . . . . 12
⊢ (𝐴 ∖ ∅) = 𝐴 |
| 22 | 21 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ ∅) ↔ 𝑥 ∈ 𝐴) |
| 23 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → dom 𝐺 = ∅) |
| 24 | | ovexd 7466 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹 supp ∅) ∈ V) |
| 25 | | cnfcom.g |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
| 26 | 5, 7, 8, 25, 15 | cantnfcl 9707 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω)) |
| 27 | 26 | simpld 494 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → E We (𝐹 supp ∅)) |
| 28 | 25 | oien 9578 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 supp ∅) ∈ V ∧ E
We (𝐹 supp ∅)) →
dom 𝐺 ≈ (𝐹 supp ∅)) |
| 29 | 24, 27, 28 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐺 ≈ (𝐹 supp ∅)) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → dom 𝐺 ≈ (𝐹 supp ∅)) |
| 31 | 23, 30 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ∅ ≈ (𝐹 supp ∅)) |
| 32 | 31 | ensymd 9045 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) ≈
∅) |
| 33 | | en0 9058 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 supp ∅) ≈ ∅
↔ (𝐹 supp ∅) =
∅) |
| 34 | 32, 33 | sylib 218 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) = ∅) |
| 35 | | ss0b 4401 |
. . . . . . . . . . . . 13
⊢ ((𝐹 supp ∅) ⊆ ∅
↔ (𝐹 supp ∅) =
∅) |
| 36 | 34, 35 | sylibr 234 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) ⊆
∅) |
| 37 | 8 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐴 ∈ On) |
| 38 | | 0ex 5307 |
. . . . . . . . . . . . 13
⊢ ∅
∈ V |
| 39 | 38 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ∅ ∈
V) |
| 40 | 19, 36, 37, 39 | suppssr 8220 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ dom 𝐺 = ∅) ∧ 𝑥 ∈ (𝐴 ∖ ∅)) → (𝐹‘𝑥) = ∅) |
| 41 | 22, 40 | sylan2br 595 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ dom 𝐺 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ∅) |
| 42 | 41 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ ∅)) |
| 43 | 20, 42 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ ∅)) |
| 44 | | fconstmpt 5747 |
. . . . . . . 8
⊢ (𝐴 × {∅}) = (𝑥 ∈ 𝐴 ↦ ∅) |
| 45 | 43, 44 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝐴 × {∅})) |
| 46 | 45 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(𝐴 × {∅}))) |
| 47 | 4 | fveq2i 6909 |
. . . . . . . 8
⊢ ((ω
CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) |
| 48 | | f1ocnvfv2 7297 |
. . . . . . . . 9
⊢
(((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) ∧ 𝐵 ∈ (ω ↑o 𝐴)) → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵) |
| 49 | 9, 13, 48 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵) |
| 50 | 47, 49 | eqtrid 2789 |
. . . . . . 7
⊢ (𝜑 → ((ω CNF 𝐴)‘𝐹) = 𝐵) |
| 51 | 50 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘𝐹) = 𝐵) |
| 52 | | peano1 7910 |
. . . . . . . . 9
⊢ ∅
∈ ω |
| 53 | 52 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈
ω) |
| 54 | 5, 7, 8, 53 | cantnf0 9715 |
. . . . . . 7
⊢ (𝜑 → ((ω CNF 𝐴)‘(𝐴 × {∅})) =
∅) |
| 55 | 54 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘(𝐴 × {∅})) =
∅) |
| 56 | 46, 51, 55 | 3eqtr3d 2785 |
. . . . 5
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐵 = ∅) |
| 57 | 3, 56 | mtand 816 |
. . . 4
⊢ (𝜑 → ¬ dom 𝐺 = ∅) |
| 58 | | nnlim 7901 |
. . . . 5
⊢ (dom
𝐺 ∈ ω →
¬ Lim dom 𝐺) |
| 59 | 26, 58 | simpl2im 503 |
. . . 4
⊢ (𝜑 → ¬ Lim dom 𝐺) |
| 60 | | ioran 986 |
. . . 4
⊢ (¬
(dom 𝐺 = ∅ ∨ Lim
dom 𝐺) ↔ (¬ dom
𝐺 = ∅ ∧ ¬ Lim
dom 𝐺)) |
| 61 | 57, 59, 60 | sylanbrc 583 |
. . 3
⊢ (𝜑 → ¬ (dom 𝐺 = ∅ ∨ Lim dom 𝐺)) |
| 62 | 25 | oicl 9569 |
. . . 4
⊢ Ord dom
𝐺 |
| 63 | | unizlim 6507 |
. . . 4
⊢ (Ord dom
𝐺 → (dom 𝐺 = ∪
dom 𝐺 ↔ (dom 𝐺 = ∅ ∨ Lim dom 𝐺))) |
| 64 | 62, 63 | ax-mp 5 |
. . 3
⊢ (dom
𝐺 = ∪ dom 𝐺 ↔ (dom 𝐺 = ∅ ∨ Lim dom 𝐺)) |
| 65 | 61, 64 | sylnibr 329 |
. 2
⊢ (𝜑 → ¬ dom 𝐺 = ∪
dom 𝐺) |
| 66 | | orduniorsuc 7850 |
. . . 4
⊢ (Ord dom
𝐺 → (dom 𝐺 = ∪
dom 𝐺 ∨ dom 𝐺 = suc ∪ dom 𝐺)) |
| 67 | 62, 66 | mp1i 13 |
. . 3
⊢ (𝜑 → (dom 𝐺 = ∪ dom 𝐺 ∨ dom 𝐺 = suc ∪ dom
𝐺)) |
| 68 | 67 | ord 865 |
. 2
⊢ (𝜑 → (¬ dom 𝐺 = ∪
dom 𝐺 → dom 𝐺 = suc ∪ dom 𝐺)) |
| 69 | 65, 68 | mpd 15 |
1
⊢ (𝜑 → dom 𝐺 = suc ∪ dom
𝐺) |