Proof of Theorem cantnflem1b
Step | Hyp | Ref
| Expression |
1 | | simprr 796 |
. . . 4
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ⊆ 𝑢) |
2 | | cantnflem1.o |
. . . . . . . 8
⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅)) |
3 | 2 | oicl 8434 |
. . . . . . 7
⊢ Ord dom
𝑂 |
4 | | cantnfs.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ On) |
5 | | suppssdm 7308 |
. . . . . . . . . . . . 13
⊢ (𝐺 supp ∅) ⊆ dom 𝐺 |
6 | | oemapval.g |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺 ∈ 𝑆) |
7 | | cantnfs.s |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
8 | | cantnfs.a |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ On) |
9 | 7, 8, 4 | cantnfs 8563 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) |
10 | 6, 9 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) |
11 | 10 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
12 | | fdm 6051 |
. . . . . . . . . . . . . 14
⊢ (𝐺:𝐵⟶𝐴 → dom 𝐺 = 𝐵) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝐺 = 𝐵) |
14 | 5, 13 | syl5sseq 3653 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵) |
15 | 4, 14 | ssexd 4805 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 supp ∅) ∈ V) |
16 | 7, 8, 4, 2, 6 | cantnfcl 8564 |
. . . . . . . . . . . 12
⊢ (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω)) |
17 | 16 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝜑 → E We (𝐺 supp ∅)) |
18 | 2 | oiiso 8442 |
. . . . . . . . . . 11
⊢ (((𝐺 supp ∅) ∈ V ∧ E
We (𝐺 supp ∅)) →
𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅))) |
19 | 15, 17, 18 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅))) |
20 | | isof1o 6573 |
. . . . . . . . . 10
⊢ (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅)) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅)) |
22 | | f1ocnv 6149 |
. . . . . . . . 9
⊢ (𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) → ◡𝑂:(𝐺 supp ∅)–1-1-onto→dom
𝑂) |
23 | | f1of 6137 |
. . . . . . . . 9
⊢ (◡𝑂:(𝐺 supp ∅)–1-1-onto→dom
𝑂 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂) |
24 | 21, 22, 23 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂) |
25 | | oemapval.t |
. . . . . . . . 9
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
26 | | oemapval.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
27 | | oemapvali.r |
. . . . . . . . 9
⊢ (𝜑 → 𝐹𝑇𝐺) |
28 | | oemapvali.x |
. . . . . . . . 9
⊢ 𝑋 = ∪
{𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} |
29 | 7, 8, 4, 25, 26, 6, 27, 28 | cantnflem1a 8582 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅)) |
30 | 24, 29 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (◡𝑂‘𝑋) ∈ dom 𝑂) |
31 | | ordelon 5747 |
. . . . . . 7
⊢ ((Ord dom
𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂) → (◡𝑂‘𝑋) ∈ On) |
32 | 3, 30, 31 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → (◡𝑂‘𝑋) ∈ On) |
33 | 32 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ∈ On) |
34 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → Ord dom 𝑂) |
35 | | ordelon 5747 |
. . . . . . . 8
⊢ ((Ord dom
𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On) |
36 | 34, 35 | sylan 488 |
. . . . . . 7
⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On) |
37 | | sucelon 7017 |
. . . . . . 7
⊢ (𝑢 ∈ On ↔ suc 𝑢 ∈ On) |
38 | 36, 37 | sylibr 224 |
. . . . . 6
⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On) |
39 | 38 | adantrr 753 |
. . . . 5
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ On) |
40 | | ontri1 5757 |
. . . . 5
⊢ (((◡𝑂‘𝑋) ∈ On ∧ 𝑢 ∈ On) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ ¬ 𝑢 ∈ (◡𝑂‘𝑋))) |
41 | 33, 39, 40 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ ¬ 𝑢 ∈ (◡𝑂‘𝑋))) |
42 | 1, 41 | mpbid 222 |
. . 3
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ¬ 𝑢 ∈ (◡𝑂‘𝑋)) |
43 | 19 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅))) |
44 | | ordtr 5737 |
. . . . . . . 8
⊢ (Ord dom
𝑂 → Tr dom 𝑂) |
45 | 3, 44 | mp1i 13 |
. . . . . . 7
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → Tr dom 𝑂) |
46 | | simprl 794 |
. . . . . . 7
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂) |
47 | | trsuc 5810 |
. . . . . . 7
⊢ ((Tr dom
𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂) |
48 | 45, 46, 47 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂) |
49 | 30 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ∈ dom 𝑂) |
50 | | isorel 6576 |
. . . . . 6
⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂)) → (𝑢 E (◡𝑂‘𝑋) ↔ (𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑋)))) |
51 | 43, 48, 49, 50 | syl12anc 1324 |
. . . . 5
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 E (◡𝑂‘𝑋) ↔ (𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑋)))) |
52 | | fvex 6201 |
. . . . . 6
⊢ (◡𝑂‘𝑋) ∈ V |
53 | 52 | epelc 5031 |
. . . . 5
⊢ (𝑢 E (◡𝑂‘𝑋) ↔ 𝑢 ∈ (◡𝑂‘𝑋)) |
54 | | fvex 6201 |
. . . . . 6
⊢ (𝑂‘(◡𝑂‘𝑋)) ∈ V |
55 | 54 | epelc 5031 |
. . . . 5
⊢ ((𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑋))) |
56 | 51, 53, 55 | 3bitr3g 302 |
. . . 4
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑋)))) |
57 | | f1ocnvfv2 6533 |
. . . . . . 7
⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) |
58 | 21, 29, 57 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) |
59 | 58 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) |
60 | 59 | eleq2d 2687 |
. . . 4
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘𝑢) ∈ 𝑋)) |
61 | 56, 60 | bitrd 268 |
. . 3
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘𝑢) ∈ 𝑋)) |
62 | 42, 61 | mtbid 314 |
. 2
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ¬ (𝑂‘𝑢) ∈ 𝑋) |
63 | 7, 8, 4, 25, 26, 6, 27, 28 | oemapvali 8581 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) |
64 | 63 | simp1d 1073 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
65 | | onelon 5748 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On) |
66 | 4, 64, 65 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ On) |
67 | 66 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ∈ On) |
68 | 4 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐵 ∈ On) |
69 | 14 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵) |
70 | 2 | oif 8435 |
. . . . . . 7
⊢ 𝑂:dom 𝑂⟶(𝐺 supp ∅) |
71 | 70 | ffvelrni 6358 |
. . . . . 6
⊢ (𝑢 ∈ dom 𝑂 → (𝑂‘𝑢) ∈ (𝐺 supp ∅)) |
72 | 48, 71 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝐺 supp ∅)) |
73 | 69, 72 | sseldd 3604 |
. . . 4
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ 𝐵) |
74 | | onelon 5748 |
. . . 4
⊢ ((𝐵 ∈ On ∧ (𝑂‘𝑢) ∈ 𝐵) → (𝑂‘𝑢) ∈ On) |
75 | 68, 73, 74 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ On) |
76 | | ontri1 5757 |
. . 3
⊢ ((𝑋 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑋 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑋)) |
77 | 67, 75, 76 | syl2anc 693 |
. 2
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑋 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑋)) |
78 | 62, 77 | mpbird 247 |
1
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ⊆ (𝑂‘𝑢)) |