Step | Hyp | Ref
| Expression |
1 | | isfinite2 8103 |
. . . . . . . 8
⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin) |
2 | | axcclem.1 |
. . . . . . . . . 10
⊢ 𝐴 = (𝑥 ∖ {∅}) |
3 | 2 | eleq1i 2679 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈
Fin) |
4 | | undif1 3995 |
. . . . . . . . . . 11
⊢ ((𝑥 ∖ {∅}) ∪
{∅}) = (𝑥 ∪
{∅}) |
5 | | snfi 7923 |
. . . . . . . . . . . 12
⊢ {∅}
∈ Fin |
6 | | unfi 8112 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∖ {∅}) ∈ Fin
∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈
Fin) |
7 | 5, 6 | mpan2 703 |
. . . . . . . . . . 11
⊢ ((𝑥 ∖ {∅}) ∈ Fin
→ ((𝑥 ∖
{∅}) ∪ {∅}) ∈ Fin) |
8 | 4, 7 | syl5eqelr 2693 |
. . . . . . . . . 10
⊢ ((𝑥 ∖ {∅}) ∈ Fin
→ (𝑥 ∪ {∅})
∈ Fin) |
9 | | ssun1 3738 |
. . . . . . . . . 10
⊢ 𝑥 ⊆ (𝑥 ∪ {∅}) |
10 | | ssfi 8065 |
. . . . . . . . . 10
⊢ (((𝑥 ∪ {∅}) ∈ Fin
∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin) |
11 | 8, 9, 10 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝑥 ∖ {∅}) ∈ Fin
→ 𝑥 ∈
Fin) |
12 | 3, 11 | sylbi 206 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin → 𝑥 ∈ Fin) |
13 | | dcomex 9152 |
. . . . . . . . . 10
⊢ ω
∈ V |
14 | | isfiniteg 8105 |
. . . . . . . . . 10
⊢ (ω
∈ V → (𝑥 ∈
Fin ↔ 𝑥 ≺
ω)) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ Fin ↔ 𝑥 ≺
ω) |
16 | | sdomnen 7870 |
. . . . . . . . 9
⊢ (𝑥 ≺ ω → ¬
𝑥 ≈
ω) |
17 | 15, 16 | sylbi 206 |
. . . . . . . 8
⊢ (𝑥 ∈ Fin → ¬ 𝑥 ≈
ω) |
18 | 1, 12, 17 | 3syl 18 |
. . . . . . 7
⊢ (𝐴 ≺ ω → ¬
𝑥 ≈
ω) |
19 | 18 | con2i 133 |
. . . . . 6
⊢ (𝑥 ≈ ω → ¬
𝐴 ≺
ω) |
20 | | sdomentr 7979 |
. . . . . . 7
⊢ ((𝐴 ≺ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≺ ω) |
21 | 20 | expcom 450 |
. . . . . 6
⊢ (𝑥 ≈ ω → (𝐴 ≺ 𝑥 → 𝐴 ≺ ω)) |
22 | 19, 21 | mtod 188 |
. . . . 5
⊢ (𝑥 ≈ ω → ¬
𝐴 ≺ 𝑥) |
23 | | vex 3176 |
. . . . . 6
⊢ 𝑥 ∈ V |
24 | | difss 3699 |
. . . . . . 7
⊢ (𝑥 ∖ {∅}) ⊆
𝑥 |
25 | 2, 24 | eqsstri 3598 |
. . . . . 6
⊢ 𝐴 ⊆ 𝑥 |
26 | | ssdomg 7887 |
. . . . . 6
⊢ (𝑥 ∈ V → (𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥)) |
27 | 23, 25, 26 | mp2 9 |
. . . . 5
⊢ 𝐴 ≼ 𝑥 |
28 | 22, 27 | jctil 558 |
. . . 4
⊢ (𝑥 ≈ ω → (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥)) |
29 | | bren2 7872 |
. . . 4
⊢ (𝐴 ≈ 𝑥 ↔ (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥)) |
30 | 28, 29 | sylibr 223 |
. . 3
⊢ (𝑥 ≈ ω → 𝐴 ≈ 𝑥) |
31 | | entr 7894 |
. . 3
⊢ ((𝐴 ≈ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≈ ω) |
32 | 30, 31 | mpancom 700 |
. 2
⊢ (𝑥 ≈ ω → 𝐴 ≈
ω) |
33 | | ensym 7891 |
. 2
⊢ (𝐴 ≈ ω → ω
≈ 𝐴) |
34 | | bren 7850 |
. . 3
⊢ (ω
≈ 𝐴 ↔
∃𝑓 𝑓:ω–1-1-onto→𝐴) |
35 | | f1of 6050 |
. . . . . . . 8
⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω⟶𝐴) |
36 | | peano1 6977 |
. . . . . . . 8
⊢ ∅
∈ ω |
37 | | ffvelrn 6265 |
. . . . . . . 8
⊢ ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω)
→ (𝑓‘∅)
∈ 𝐴) |
38 | 35, 36, 37 | sylancl 693 |
. . . . . . 7
⊢ (𝑓:ω–1-1-onto→𝐴 → (𝑓‘∅) ∈ 𝐴) |
39 | | eldifn 3695 |
. . . . . . . . 9
⊢ ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬
(𝑓‘∅) ∈
{∅}) |
40 | 39, 2 | eleq2s 2706 |
. . . . . . . 8
⊢ ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈
{∅}) |
41 | | fvex 6113 |
. . . . . . . . . . 11
⊢ (𝑓‘∅) ∈
V |
42 | 41 | elsn 4140 |
. . . . . . . . . 10
⊢ ((𝑓‘∅) ∈ {∅}
↔ (𝑓‘∅) =
∅) |
43 | 42 | notbii 309 |
. . . . . . . . 9
⊢ (¬
(𝑓‘∅) ∈
{∅} ↔ ¬ (𝑓‘∅) = ∅) |
44 | | neq0 3889 |
. . . . . . . . 9
⊢ (¬
(𝑓‘∅) = ∅
↔ ∃𝑐 𝑐 ∈ (𝑓‘∅)) |
45 | 43, 44 | bitr2i 264 |
. . . . . . . 8
⊢
(∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈
{∅}) |
46 | 40, 45 | sylibr 223 |
. . . . . . 7
⊢ ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅)) |
47 | 38, 46 | syl 17 |
. . . . . 6
⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅)) |
48 | | elunii 4377 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 ∈ ∪ 𝐴) |
49 | 38, 48 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝑐 ∈ ∪ 𝐴) |
50 | 35 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → (𝑓‘𝑛) ∈ 𝐴) |
51 | | difabs 3851 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∖ {∅}) ∖
{∅}) = (𝑥 ∖
{∅}) |
52 | 2 | difeq1i 3686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖
{∅}) |
53 | 51, 52, 2 | 3eqtr4i 2642 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∖ {∅}) = 𝐴 |
54 | | pwuni 4825 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 |
55 | | ssdif 3707 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ⊆ 𝒫 ∪ 𝐴
→ (𝐴 ∖
{∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅})) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∖ {∅}) ⊆
(𝒫 ∪ 𝐴 ∖ {∅}) |
57 | 53, 56 | eqsstr3i 3599 |
. . . . . . . . . . . . . . . 16
⊢ 𝐴 ⊆ (𝒫 ∪ 𝐴
∖ {∅}) |
58 | 57 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑛) ∈ 𝐴 → (𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴
∖ {∅})) |
59 | 58 | ralrimivw 2950 |
. . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑛) ∈ 𝐴 → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴
∖ {∅})) |
60 | 50, 59 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴
∖ {∅})) |
61 | 60 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝑓:ω–1-1-onto→𝐴 → ∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴
∖ {∅})) |
62 | | axcclem.2 |
. . . . . . . . . . . . 13
⊢ 𝐹 = (𝑛 ∈ ω, 𝑦 ∈ ∪ 𝐴 ↦ (𝑓‘𝑛)) |
63 | 62 | fmpt2 7126 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω ∀𝑦 ∈
∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴
∖ {∅}) ↔ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴
∖ {∅})) |
64 | 61, 63 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝑓:ω–1-1-onto→𝐴 → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴
∖ {∅})) |
65 | 64 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴
∖ {∅})) |
66 | | difexg 4735 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ V → (𝑥 ∖ {∅}) ∈
V) |
67 | 23, 66 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∖ {∅}) ∈
V |
68 | 2, 67 | eqeltri 2684 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈ V |
69 | 68 | uniex 6851 |
. . . . . . . . . . 11
⊢ ∪ 𝐴
∈ V |
70 | 69 | axdc4 9161 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ∪ 𝐴
∧ 𝐹:(ω ×
∪ 𝐴)⟶(𝒫 ∪ 𝐴
∖ {∅})) → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
71 | 49, 65, 70 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
72 | | 3simpb 1052 |
. . . . . . . . . 10
⊢ ((ℎ:ω⟶∪ 𝐴
∧ (ℎ‘∅) =
𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
73 | 72 | eximi 1752 |
. . . . . . . . 9
⊢
(∃ℎ(ℎ:ω⟶∪ 𝐴
∧ (ℎ‘∅) =
𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
74 | 71, 73 | syl 17 |
. . . . . . . 8
⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
75 | 74 | ex 449 |
. . . . . . 7
⊢ (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))) |
76 | 75 | exlimiv 1845 |
. . . . . 6
⊢
(∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))) |
77 | 47, 76 | mpcom 37 |
. . . . 5
⊢ (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
78 | | velsn 4141 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {∅} ↔ 𝑧 = ∅) |
79 | 78 | necon3bbii 2829 |
. . . . . . . . . 10
⊢ (¬
𝑧 ∈ {∅} ↔
𝑧 ≠
∅) |
80 | 2 | eleq2i 2680 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ (𝑥 ∖ {∅})) |
81 | | eldif 3550 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅})) |
82 | 80, 81 | sylbbr 225 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧 ∈ 𝐴) |
83 | 79, 82 | sylan2br 492 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝐴) |
84 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑓:ω–1-1-onto→𝐴) |
85 | | f1ofo 6057 |
. . . . . . . . . . . . . 14
⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω–onto→𝐴) |
86 | | foelrn 6286 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:ω–onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖)) |
87 | 85, 86 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖)) |
88 | | suceq 5707 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖) |
89 | 88 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖)) |
90 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 = 𝑖 → 𝑘 = 𝑖) |
91 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 = 𝑖 → (ℎ‘𝑘) = (ℎ‘𝑖)) |
92 | 90, 91 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑖 → (𝑘𝐹(ℎ‘𝑘)) = (𝑖𝐹(ℎ‘𝑖))) |
93 | 89, 92 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))) |
94 | 93 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ ω →
(∀𝑘 ∈ ω
(ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))) |
95 | 94 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))) |
96 | 95 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))) |
97 | 96 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))) |
98 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = (𝑓‘𝑖) ↔ (𝑓‘𝑖) = 𝑧) |
99 | | f1ocnvfv 6434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → ((𝑓‘𝑖) = 𝑧 → (◡𝑓‘𝑧) = 𝑖)) |
100 | 98, 99 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖)) |
101 | 100 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖)) |
102 | 101 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → (◡𝑓‘𝑧) = 𝑖) |
103 | 102 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧)) |
104 | 103 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧)) |
105 | | suceq 5707 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = (◡𝑓‘𝑧) → suc 𝑖 = suc (◡𝑓‘𝑧)) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → suc 𝑖 = suc (◡𝑓‘𝑧)) |
107 | 106 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) = (ℎ‘suc (◡𝑓‘𝑧))) |
108 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑖 ∈ ω)
→ 𝑖 ∈
ω) |
109 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑖 ∈ ω)
→ (ℎ‘𝑖) ∈ ∪ 𝐴) |
110 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖)) |
111 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (ℎ‘𝑖) → (𝑓‘𝑖) = (𝑓‘𝑖)) |
112 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓‘𝑖) ∈ V |
113 | 110, 111,
62, 112 | ovmpt2 6694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ ω ∧ (ℎ‘𝑖) ∈ ∪ 𝐴) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖)) |
114 | 108, 109,
113 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑖 ∈ ω)
→ (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖)) |
115 | 114 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖)) |
116 | 115 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖)) |
117 | 97, 107, 116 | 3eltr3d 2702 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc (◡𝑓‘𝑧)) ∈ (𝑓‘𝑖)) |
118 | 35 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴) |
119 | 118 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴) |
120 | 119 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑓‘𝑖) ∈ 𝐴) |
121 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (𝑓‘𝑖) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴)) |
122 | 121 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴)) |
123 | 120, 122 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 ∈ 𝐴) |
124 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑧 → (◡𝑓‘𝑤) = (◡𝑓‘𝑧)) |
125 | | suceq 5707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((◡𝑓‘𝑤) = (◡𝑓‘𝑧) → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧)) |
126 | 124, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑧 → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧)) |
127 | 126 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑧 → (ℎ‘suc (◡𝑓‘𝑤)) = (ℎ‘suc (◡𝑓‘𝑧))) |
128 | | axcclem.3 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐺 = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) |
129 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ‘suc (◡𝑓‘𝑧)) ∈ V |
130 | 127, 128,
129 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝐴 → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧))) |
131 | 123, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧))) |
132 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 = (𝑓‘𝑖)) |
133 | 117, 131,
132 | 3eltr4d 2703 |
. . . . . . . . . . . . . . . . . 18
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) ∈ 𝑧) |
134 | 133 | 3exp 1256 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝑧 = (𝑓‘𝑖) → (𝐺‘𝑧) ∈ 𝑧))) |
135 | 134 | com3r 85 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑓‘𝑖) → ((ℎ:ω⟶∪
𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))) |
136 | 135 | 3expd 1276 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪
𝐴 → (𝑓:ω–1-1-onto→𝐴 → (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))))) |
137 | 136 | com4r 92 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ω → (𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪
𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))))) |
138 | 137 | rexlimiv 3009 |
. . . . . . . . . . . . 13
⊢
(∃𝑖 ∈
ω 𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪
𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))) |
139 | 87, 138 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → (ℎ:ω⟶∪
𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))) |
140 | 84, 139 | mpid 43 |
. . . . . . . . . . 11
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → (ℎ:ω⟶∪
𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))) |
141 | 140 | impd 446 |
. . . . . . . . . 10
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ((ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (𝐺‘𝑧) ∈ 𝑧)) |
142 | 141 | impancom 455 |
. . . . . . . . 9
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝐴 → (𝐺‘𝑧) ∈ 𝑧)) |
143 | 83, 142 | syl5 33 |
. . . . . . . 8
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (𝐺‘𝑧) ∈ 𝑧)) |
144 | 143 | expd 451 |
. . . . . . 7
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))) |
145 | 144 | ralrimiv 2948 |
. . . . . 6
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)) |
146 | | fvrn0 6126 |
. . . . . . . . . . 11
⊢ (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) |
147 | 146 | rgenw 2908 |
. . . . . . . . . 10
⊢
∀𝑤 ∈
𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) |
148 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) |
149 | 148 | fmpt 6289 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) ↔ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅})) |
150 | 147, 149 | mpbi 219 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}) |
151 | | vex 3176 |
. . . . . . . . . . 11
⊢ ℎ ∈ V |
152 | 151 | rnex 6992 |
. . . . . . . . . 10
⊢ ran ℎ ∈ V |
153 | | p0ex 4779 |
. . . . . . . . . 10
⊢ {∅}
∈ V |
154 | 152, 153 | unex 6854 |
. . . . . . . . 9
⊢ (ran
ℎ ∪ {∅}) ∈
V |
155 | | fex2 7014 |
. . . . . . . . 9
⊢ (((𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V) |
156 | 150, 68, 154, 155 | mp3an 1416 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V |
157 | 128, 156 | eqeltri 2684 |
. . . . . . 7
⊢ 𝐺 ∈ V |
158 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑔‘𝑧) = (𝐺‘𝑧)) |
159 | 158 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝑔‘𝑧) ∈ 𝑧 ↔ (𝐺‘𝑧) ∈ 𝑧)) |
160 | 159 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))) |
161 | 160 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))) |
162 | 157, 161 | spcev 3273 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |
163 | 145, 162 | syl 17 |
. . . . 5
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |
164 | 77, 163 | exlimddv 1850 |
. . . 4
⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |
165 | 164 | exlimiv 1845 |
. . 3
⊢
(∃𝑓 𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |
166 | 34, 165 | sylbi 206 |
. 2
⊢ (ω
≈ 𝐴 →
∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |
167 | 32, 33, 166 | 3syl 18 |
1
⊢ (𝑥 ≈ ω →
∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |