Proof of Theorem cantnfp1lem2
Step | Hyp | Ref
| Expression |
1 | | cantnfp1.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
2 | | cantnfp1.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝐴) |
3 | | iftrue 4092 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑋 → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) = 𝑌) |
4 | | cantnfp1.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) |
5 | 3, 4 | fvmptg 6280 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴) → (𝐹‘𝑋) = 𝑌) |
6 | 1, 2, 5 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑋) = 𝑌) |
7 | | cantnfp1.e |
. . . . . . . . 9
⊢ (𝜑 → ∅ ∈ 𝑌) |
8 | | cantnfs.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ On) |
9 | | onelon 5748 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑌 ∈ 𝐴) → 𝑌 ∈ On) |
10 | 8, 2, 9 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ On) |
11 | | on0eln0 5780 |
. . . . . . . . . 10
⊢ (𝑌 ∈ On → (∅
∈ 𝑌 ↔ 𝑌 ≠ ∅)) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅)) |
13 | 7, 12 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ≠ ∅) |
14 | 6, 13 | eqnetrd 2861 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑋) ≠ ∅) |
15 | 2 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → 𝑌 ∈ 𝐴) |
16 | | cantnfp1.g |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ 𝑆) |
17 | | cantnfs.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
18 | | cantnfs.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ On) |
19 | 17, 8, 18 | cantnfs 8563 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) |
20 | 16, 19 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) |
21 | 20 | simpld 475 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
22 | 21 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → (𝐺‘𝑡) ∈ 𝐴) |
23 | 15, 22 | ifcld 4131 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) ∈ 𝐴) |
24 | 23, 4 | fmptd 6385 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐵⟶𝐴) |
25 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐹:𝐵⟶𝐴 → 𝐹 Fn 𝐵) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝐵) |
27 | | 0ex 4790 |
. . . . . . . . 9
⊢ ∅
∈ V |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈
V) |
29 | | elsuppfn 7303 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ≠ ∅))) |
30 | 26, 18, 28, 29 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ≠ ∅))) |
31 | 1, 14, 30 | mpbir2and 957 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐹 supp ∅)) |
32 | | n0i 3920 |
. . . . . 6
⊢ (𝑋 ∈ (𝐹 supp ∅) → ¬ (𝐹 supp ∅) =
∅) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → ¬ (𝐹 supp ∅) = ∅) |
34 | | suppssdm 7308 |
. . . . . . . . 9
⊢ (𝐹 supp ∅) ⊆ dom 𝐹 |
35 | 4, 23 | dmmptd 6024 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐵) |
36 | 34, 35 | syl5sseq 3653 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐵) |
37 | 18, 36 | ssexd 4805 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp ∅) ∈ V) |
38 | | cantnfp1.o |
. . . . . . . . 9
⊢ 𝑂 = OrdIso( E , (𝐹 supp ∅)) |
39 | | cantnfp1.s |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋) |
40 | 17, 8, 18, 16, 1, 2, 39, 4 | cantnfp1lem1 8575 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
41 | 17, 8, 18, 38, 40 | cantnfcl 8564 |
. . . . . . . 8
⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝑂 ∈ ω)) |
42 | 41 | simpld 475 |
. . . . . . 7
⊢ (𝜑 → E We (𝐹 supp ∅)) |
43 | 38 | oien 8443 |
. . . . . . 7
⊢ (((𝐹 supp ∅) ∈ V ∧ E
We (𝐹 supp ∅)) →
dom 𝑂 ≈ (𝐹 supp ∅)) |
44 | 37, 42, 43 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → dom 𝑂 ≈ (𝐹 supp ∅)) |
45 | | breq1 4656 |
. . . . . . 7
⊢ (dom
𝑂 = ∅ → (dom
𝑂 ≈ (𝐹 supp ∅) ↔ ∅
≈ (𝐹 supp
∅))) |
46 | | ensymb 8004 |
. . . . . . . 8
⊢ (∅
≈ (𝐹 supp ∅)
↔ (𝐹 supp ∅)
≈ ∅) |
47 | | en0 8019 |
. . . . . . . 8
⊢ ((𝐹 supp ∅) ≈ ∅
↔ (𝐹 supp ∅) =
∅) |
48 | 46, 47 | bitri 264 |
. . . . . . 7
⊢ (∅
≈ (𝐹 supp ∅)
↔ (𝐹 supp ∅) =
∅) |
49 | 45, 48 | syl6bb 276 |
. . . . . 6
⊢ (dom
𝑂 = ∅ → (dom
𝑂 ≈ (𝐹 supp ∅) ↔ (𝐹 supp ∅) =
∅)) |
50 | 44, 49 | syl5ibcom 235 |
. . . . 5
⊢ (𝜑 → (dom 𝑂 = ∅ → (𝐹 supp ∅) = ∅)) |
51 | 33, 50 | mtod 189 |
. . . 4
⊢ (𝜑 → ¬ dom 𝑂 = ∅) |
52 | 41 | simprd 479 |
. . . . 5
⊢ (𝜑 → dom 𝑂 ∈ ω) |
53 | | nnlim 7078 |
. . . . 5
⊢ (dom
𝑂 ∈ ω →
¬ Lim dom 𝑂) |
54 | 52, 53 | syl 17 |
. . . 4
⊢ (𝜑 → ¬ Lim dom 𝑂) |
55 | | ioran 511 |
. . . 4
⊢ (¬
(dom 𝑂 = ∅ ∨ Lim
dom 𝑂) ↔ (¬ dom
𝑂 = ∅ ∧ ¬ Lim
dom 𝑂)) |
56 | 51, 54, 55 | sylanbrc 698 |
. . 3
⊢ (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)) |
57 | | nnord 7073 |
. . . 4
⊢ (dom
𝑂 ∈ ω → Ord
dom 𝑂) |
58 | | unizlim 5844 |
. . . 4
⊢ (Ord dom
𝑂 → (dom 𝑂 = ∪
dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))) |
59 | 52, 57, 58 | 3syl 18 |
. . 3
⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))) |
60 | 56, 59 | mtbird 315 |
. 2
⊢ (𝜑 → ¬ dom 𝑂 = ∪
dom 𝑂) |
61 | | orduniorsuc 7030 |
. . . 4
⊢ (Ord dom
𝑂 → (dom 𝑂 = ∪
dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂)) |
62 | 52, 57, 61 | 3syl 18 |
. . 3
⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom
𝑂)) |
63 | 62 | ord 392 |
. 2
⊢ (𝜑 → (¬ dom 𝑂 = ∪
dom 𝑂 → dom 𝑂 = suc ∪ dom 𝑂)) |
64 | 60, 63 | mpd 15 |
1
⊢ (𝜑 → dom 𝑂 = suc ∪ dom
𝑂) |