Proof of Theorem cnfcom2lem
Step | Hyp | Ref
| Expression |
1 | | cnfcom2.1 |
. . . . . 6
⊢ (𝜑 → ∅ ∈ 𝐵) |
2 | | n0i 3920 |
. . . . . 6
⊢ (∅
∈ 𝐵 → ¬ 𝐵 = ∅) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → ¬ 𝐵 = ∅) |
4 | | cnfcom.f |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) |
5 | | cnfcom.s |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 = dom (ω CNF 𝐴) |
6 | | omelon 8543 |
. . . . . . . . . . . . . . . . . 18
⊢ ω
∈ On |
7 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ω ∈
On) |
8 | | cnfcom.a |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ On) |
9 | 5, 7, 8 | cantnff1o 8593 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴)) |
10 | | f1ocnv 6149 |
. . . . . . . . . . . . . . . 16
⊢ ((ω
CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴) → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆) |
11 | | f1of 6137 |
. . . . . . . . . . . . . . . 16
⊢ (◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆) |
13 | | cnfcom.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜
𝐴)) |
14 | 12, 13 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆) |
15 | 4, 14 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
16 | 5, 7, 8 | cantnfs 8563 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))) |
17 | 15, 16 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)) |
18 | 17 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶ω) |
19 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹:𝐴⟶ω) |
20 | 19 | feqmptd 6249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
21 | | dif0 3950 |
. . . . . . . . . . . 12
⊢ (𝐴 ∖ ∅) = 𝐴 |
22 | 21 | eleq2i 2693 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ ∅) ↔ 𝑥 ∈ 𝐴) |
23 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → dom 𝐺 = ∅) |
24 | | suppssdm 7308 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 supp ∅) ⊆ dom 𝐹 |
25 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹:𝐴⟶ω → dom 𝐹 = 𝐴) |
26 | 18, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → dom 𝐹 = 𝐴) |
27 | 24, 26 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴) |
28 | 8, 27 | ssexd 4805 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹 supp ∅) ∈ V) |
29 | | cnfcom.g |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
30 | 5, 7, 8, 29, 15 | cantnfcl 8564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω)) |
31 | 30 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → E We (𝐹 supp ∅)) |
32 | 29 | oien 8443 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 supp ∅) ∈ V ∧ E
We (𝐹 supp ∅)) →
dom 𝐺 ≈ (𝐹 supp ∅)) |
33 | 28, 31, 32 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐺 ≈ (𝐹 supp ∅)) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → dom 𝐺 ≈ (𝐹 supp ∅)) |
35 | 23, 34 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ∅ ≈ (𝐹 supp ∅)) |
36 | 35 | ensymd 8007 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) ≈
∅) |
37 | | en0 8019 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 supp ∅) ≈ ∅
↔ (𝐹 supp ∅) =
∅) |
38 | 36, 37 | sylib 208 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) = ∅) |
39 | | ss0b 3973 |
. . . . . . . . . . . . 13
⊢ ((𝐹 supp ∅) ⊆ ∅
↔ (𝐹 supp ∅) =
∅) |
40 | 38, 39 | sylibr 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) ⊆
∅) |
41 | 8 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐴 ∈ On) |
42 | | 0ex 4790 |
. . . . . . . . . . . . 13
⊢ ∅
∈ V |
43 | 42 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ∅ ∈
V) |
44 | 19, 40, 41, 43 | suppssr 7326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ dom 𝐺 = ∅) ∧ 𝑥 ∈ (𝐴 ∖ ∅)) → (𝐹‘𝑥) = ∅) |
45 | 22, 44 | sylan2br 493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ dom 𝐺 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ∅) |
46 | 45 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ ∅)) |
47 | 20, 46 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ ∅)) |
48 | | fconstmpt 5163 |
. . . . . . . 8
⊢ (𝐴 × {∅}) = (𝑥 ∈ 𝐴 ↦ ∅) |
49 | 47, 48 | syl6eqr 2674 |
. . . . . . 7
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝐴 × {∅})) |
50 | 49 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(𝐴 × {∅}))) |
51 | 4 | fveq2i 6194 |
. . . . . . . 8
⊢ ((ω
CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) |
52 | | f1ocnvfv2 6533 |
. . . . . . . . 9
⊢
(((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴) ∧ 𝐵 ∈ (ω ↑𝑜
𝐴)) → ((ω CNF
𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵) |
53 | 9, 13, 52 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵) |
54 | 51, 53 | syl5eq 2668 |
. . . . . . 7
⊢ (𝜑 → ((ω CNF 𝐴)‘𝐹) = 𝐵) |
55 | 54 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘𝐹) = 𝐵) |
56 | | peano1 7085 |
. . . . . . . . 9
⊢ ∅
∈ ω |
57 | 56 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈
ω) |
58 | 5, 7, 8, 57 | cantnf0 8572 |
. . . . . . 7
⊢ (𝜑 → ((ω CNF 𝐴)‘(𝐴 × {∅})) =
∅) |
59 | 58 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘(𝐴 × {∅})) =
∅) |
60 | 50, 55, 59 | 3eqtr3d 2664 |
. . . . 5
⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐵 = ∅) |
61 | 3, 60 | mtand 691 |
. . . 4
⊢ (𝜑 → ¬ dom 𝐺 = ∅) |
62 | 30 | simprd 479 |
. . . . 5
⊢ (𝜑 → dom 𝐺 ∈ ω) |
63 | | nnlim 7078 |
. . . . 5
⊢ (dom
𝐺 ∈ ω →
¬ Lim dom 𝐺) |
64 | 62, 63 | syl 17 |
. . . 4
⊢ (𝜑 → ¬ Lim dom 𝐺) |
65 | | ioran 511 |
. . . 4
⊢ (¬
(dom 𝐺 = ∅ ∨ Lim
dom 𝐺) ↔ (¬ dom
𝐺 = ∅ ∧ ¬ Lim
dom 𝐺)) |
66 | 61, 64, 65 | sylanbrc 698 |
. . 3
⊢ (𝜑 → ¬ (dom 𝐺 = ∅ ∨ Lim dom 𝐺)) |
67 | 29 | oicl 8434 |
. . . 4
⊢ Ord dom
𝐺 |
68 | | unizlim 5844 |
. . . 4
⊢ (Ord dom
𝐺 → (dom 𝐺 = ∪
dom 𝐺 ↔ (dom 𝐺 = ∅ ∨ Lim dom 𝐺))) |
69 | 67, 68 | ax-mp 5 |
. . 3
⊢ (dom
𝐺 = ∪ dom 𝐺 ↔ (dom 𝐺 = ∅ ∨ Lim dom 𝐺)) |
70 | 66, 69 | sylnibr 319 |
. 2
⊢ (𝜑 → ¬ dom 𝐺 = ∪
dom 𝐺) |
71 | | orduniorsuc 7030 |
. . . 4
⊢ (Ord dom
𝐺 → (dom 𝐺 = ∪
dom 𝐺 ∨ dom 𝐺 = suc ∪ dom 𝐺)) |
72 | 67, 71 | mp1i 13 |
. . 3
⊢ (𝜑 → (dom 𝐺 = ∪ dom 𝐺 ∨ dom 𝐺 = suc ∪ dom
𝐺)) |
73 | 72 | ord 392 |
. 2
⊢ (𝜑 → (¬ dom 𝐺 = ∪
dom 𝐺 → dom 𝐺 = suc ∪ dom 𝐺)) |
74 | 70, 73 | mpd 15 |
1
⊢ (𝜑 → dom 𝐺 = suc ∪ dom
𝐺) |