Step | Hyp | Ref
| Expression |
1 | | isfinite2 8851 |
. . . . . . . 8
⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin) |
2 | | axcclem.1 |
. . . . . . . . . 10
⊢ 𝐴 = (𝑥 ∖ {∅}) |
3 | 2 | eleq1i 2823 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈
Fin) |
4 | | undif1 4366 |
. . . . . . . . . . 11
⊢ ((𝑥 ∖ {∅}) ∪
{∅}) = (𝑥 ∪
{∅}) |
5 | | snfi 8643 |
. . . . . . . . . . . 12
⊢ {∅}
∈ Fin |
6 | | unfi 8772 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∖ {∅}) ∈ Fin
∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈
Fin) |
7 | 5, 6 | mpan2 691 |
. . . . . . . . . . 11
⊢ ((𝑥 ∖ {∅}) ∈ Fin
→ ((𝑥 ∖
{∅}) ∪ {∅}) ∈ Fin) |
8 | 4, 7 | eqeltrrid 2838 |
. . . . . . . . . 10
⊢ ((𝑥 ∖ {∅}) ∈ Fin
→ (𝑥 ∪ {∅})
∈ Fin) |
9 | | ssun1 4063 |
. . . . . . . . . 10
⊢ 𝑥 ⊆ (𝑥 ∪ {∅}) |
10 | | ssfi 8773 |
. . . . . . . . . 10
⊢ (((𝑥 ∪ {∅}) ∈ Fin
∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin) |
11 | 8, 9, 10 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝑥 ∖ {∅}) ∈ Fin
→ 𝑥 ∈
Fin) |
12 | 3, 11 | sylbi 220 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin → 𝑥 ∈ Fin) |
13 | | dcomex 9948 |
. . . . . . . . . 10
⊢ ω
∈ V |
14 | | isfiniteg 8853 |
. . . . . . . . . 10
⊢ (ω
∈ V → (𝑥 ∈
Fin ↔ 𝑥 ≺
ω)) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ Fin ↔ 𝑥 ≺
ω) |
16 | | sdomnen 8585 |
. . . . . . . . 9
⊢ (𝑥 ≺ ω → ¬
𝑥 ≈
ω) |
17 | 15, 16 | sylbi 220 |
. . . . . . . 8
⊢ (𝑥 ∈ Fin → ¬ 𝑥 ≈
ω) |
18 | 1, 12, 17 | 3syl 18 |
. . . . . . 7
⊢ (𝐴 ≺ ω → ¬
𝑥 ≈
ω) |
19 | 18 | con2i 141 |
. . . . . 6
⊢ (𝑥 ≈ ω → ¬
𝐴 ≺
ω) |
20 | | sdomentr 8702 |
. . . . . . 7
⊢ ((𝐴 ≺ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≺ ω) |
21 | 20 | expcom 417 |
. . . . . 6
⊢ (𝑥 ≈ ω → (𝐴 ≺ 𝑥 → 𝐴 ≺ ω)) |
22 | 19, 21 | mtod 201 |
. . . . 5
⊢ (𝑥 ≈ ω → ¬
𝐴 ≺ 𝑥) |
23 | | vex 3402 |
. . . . . 6
⊢ 𝑥 ∈ V |
24 | | difss 4023 |
. . . . . . 7
⊢ (𝑥 ∖ {∅}) ⊆
𝑥 |
25 | 2, 24 | eqsstri 3912 |
. . . . . 6
⊢ 𝐴 ⊆ 𝑥 |
26 | | ssdomg 8602 |
. . . . . 6
⊢ (𝑥 ∈ V → (𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥)) |
27 | 23, 25, 26 | mp2 9 |
. . . . 5
⊢ 𝐴 ≼ 𝑥 |
28 | 22, 27 | jctil 523 |
. . . 4
⊢ (𝑥 ≈ ω → (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥)) |
29 | | bren2 8587 |
. . . 4
⊢ (𝐴 ≈ 𝑥 ↔ (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥)) |
30 | 28, 29 | sylibr 237 |
. . 3
⊢ (𝑥 ≈ ω → 𝐴 ≈ 𝑥) |
31 | | entr 8608 |
. . 3
⊢ ((𝐴 ≈ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≈ ω) |
32 | 30, 31 | mpancom 688 |
. 2
⊢ (𝑥 ≈ ω → 𝐴 ≈
ω) |
33 | | ensym 8605 |
. 2
⊢ (𝐴 ≈ ω → ω
≈ 𝐴) |
34 | | bren 8565 |
. . 3
⊢ (ω
≈ 𝐴 ↔
∃𝑓 𝑓:ω–1-1-onto→𝐴) |
35 | | f1of 6619 |
. . . . . . . 8
⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω⟶𝐴) |
36 | | peano1 7621 |
. . . . . . . 8
⊢ ∅
∈ ω |
37 | | ffvelrn 6860 |
. . . . . . . 8
⊢ ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω)
→ (𝑓‘∅)
∈ 𝐴) |
38 | 35, 36, 37 | sylancl 589 |
. . . . . . 7
⊢ (𝑓:ω–1-1-onto→𝐴 → (𝑓‘∅) ∈ 𝐴) |
39 | | eldifn 4019 |
. . . . . . . . 9
⊢ ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬
(𝑓‘∅) ∈
{∅}) |
40 | 39, 2 | eleq2s 2851 |
. . . . . . . 8
⊢ ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈
{∅}) |
41 | | fvex 6688 |
. . . . . . . . . . 11
⊢ (𝑓‘∅) ∈
V |
42 | 41 | elsn 4532 |
. . . . . . . . . 10
⊢ ((𝑓‘∅) ∈ {∅}
↔ (𝑓‘∅) =
∅) |
43 | 42 | notbii 323 |
. . . . . . . . 9
⊢ (¬
(𝑓‘∅) ∈
{∅} ↔ ¬ (𝑓‘∅) = ∅) |
44 | | neq0 4235 |
. . . . . . . . 9
⊢ (¬
(𝑓‘∅) = ∅
↔ ∃𝑐 𝑐 ∈ (𝑓‘∅)) |
45 | 43, 44 | bitr2i 279 |
. . . . . . . 8
⊢
(∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈
{∅}) |
46 | 40, 45 | sylibr 237 |
. . . . . . 7
⊢ ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅)) |
47 | 38, 46 | syl 17 |
. . . . . 6
⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅)) |
48 | | elunii 4802 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 ∈ ∪ 𝐴) |
49 | 38, 48 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝑐 ∈ ∪ 𝐴) |
50 | 35 | ffvelrnda 6862 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → (𝑓‘𝑛) ∈ 𝐴) |
51 | | difabs 4185 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∖ {∅}) ∖
{∅}) = (𝑥 ∖
{∅}) |
52 | 2 | difeq1i 4010 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖
{∅}) |
53 | 51, 52, 2 | 3eqtr4i 2771 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∖ {∅}) = 𝐴 |
54 | | pwuni 4836 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 |
55 | | ssdif 4031 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ⊆ 𝒫 ∪ 𝐴
→ (𝐴 ∖
{∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅})) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∖ {∅}) ⊆
(𝒫 ∪ 𝐴 ∖ {∅}) |
57 | 53, 56 | eqsstrri 3913 |
. . . . . . . . . . . . . . . 16
⊢ 𝐴 ⊆ (𝒫 ∪ 𝐴
∖ {∅}) |
58 | 57 | sseli 3874 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑛) ∈ 𝐴 → (𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴
∖ {∅})) |
59 | 58 | ralrimivw 3097 |
. . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑛) ∈ 𝐴 → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴
∖ {∅})) |
60 | 50, 59 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴
∖ {∅})) |
61 | 60 | ralrimiva 3096 |
. . . . . . . . . . . 12
⊢ (𝑓:ω–1-1-onto→𝐴 → ∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴
∖ {∅})) |
62 | | axcclem.2 |
. . . . . . . . . . . . 13
⊢ 𝐹 = (𝑛 ∈ ω, 𝑦 ∈ ∪ 𝐴 ↦ (𝑓‘𝑛)) |
63 | 62 | fmpo 7792 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω ∀𝑦 ∈
∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴
∖ {∅}) ↔ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴
∖ {∅})) |
64 | 61, 63 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝑓:ω–1-1-onto→𝐴 → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴
∖ {∅})) |
65 | 64 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴
∖ {∅})) |
66 | 23 | difexi 5197 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∖ {∅}) ∈
V |
67 | 2, 66 | eqeltri 2829 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈ V |
68 | 67 | uniex 7486 |
. . . . . . . . . . 11
⊢ ∪ 𝐴
∈ V |
69 | 68 | axdc4 9957 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ∪ 𝐴
∧ 𝐹:(ω ×
∪ 𝐴)⟶(𝒫 ∪ 𝐴
∖ {∅})) → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
70 | 49, 65, 69 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
71 | | 3simpb 1150 |
. . . . . . . . . 10
⊢ ((ℎ:ω⟶∪ 𝐴
∧ (ℎ‘∅) =
𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
72 | 71 | eximi 1841 |
. . . . . . . . 9
⊢
(∃ℎ(ℎ:ω⟶∪ 𝐴
∧ (ℎ‘∅) =
𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
73 | 70, 72 | syl 17 |
. . . . . . . 8
⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
74 | 73 | ex 416 |
. . . . . . 7
⊢ (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))) |
75 | 74 | exlimiv 1936 |
. . . . . 6
⊢
(∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))) |
76 | 47, 75 | mpcom 38 |
. . . . 5
⊢ (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) |
77 | | velsn 4533 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {∅} ↔ 𝑧 = ∅) |
78 | 77 | necon3bbii 2981 |
. . . . . . . . . 10
⊢ (¬
𝑧 ∈ {∅} ↔
𝑧 ≠
∅) |
79 | 2 | eleq2i 2824 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ (𝑥 ∖ {∅})) |
80 | | eldif 3854 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅})) |
81 | 79, 80 | sylbbr 239 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧 ∈ 𝐴) |
82 | 78, 81 | sylan2br 598 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝐴) |
83 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑓:ω–1-1-onto→𝐴) |
84 | | f1ofo 6626 |
. . . . . . . . . . . . . 14
⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω–onto→𝐴) |
85 | | foelrn 6883 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:ω–onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖)) |
86 | 84, 85 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖)) |
87 | | suceq 6238 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖) |
88 | 87 | fveq2d 6679 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖)) |
89 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 = 𝑖 → 𝑘 = 𝑖) |
90 | | fveq2 6675 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 = 𝑖 → (ℎ‘𝑘) = (ℎ‘𝑖)) |
91 | 89, 90 | oveq12d 7189 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑖 → (𝑘𝐹(ℎ‘𝑘)) = (𝑖𝐹(ℎ‘𝑖))) |
92 | 88, 91 | eleq12d 2827 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))) |
93 | 92 | rspcv 3522 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ ω →
(∀𝑘 ∈ ω
(ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))) |
94 | 93 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))) |
95 | 94 | imp 410 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))) |
96 | 95 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))) |
97 | | eqcom 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = (𝑓‘𝑖) ↔ (𝑓‘𝑖) = 𝑧) |
98 | | f1ocnvfv 7047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → ((𝑓‘𝑖) = 𝑧 → (◡𝑓‘𝑧) = 𝑖)) |
99 | 97, 98 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖)) |
100 | 99 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖)) |
101 | 100 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → (◡𝑓‘𝑧) = 𝑖) |
102 | 101 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧)) |
103 | 102 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧)) |
104 | | suceq 6238 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = (◡𝑓‘𝑧) → suc 𝑖 = suc (◡𝑓‘𝑧)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → suc 𝑖 = suc (◡𝑓‘𝑧)) |
106 | 105 | fveq2d 6679 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) = (ℎ‘suc (◡𝑓‘𝑧))) |
107 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑖 ∈ ω)
→ 𝑖 ∈
ω) |
108 | | ffvelrn 6860 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑖 ∈ ω)
→ (ℎ‘𝑖) ∈ ∪ 𝐴) |
109 | | fveq2 6675 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖)) |
110 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (ℎ‘𝑖) → (𝑓‘𝑖) = (𝑓‘𝑖)) |
111 | | fvex 6688 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓‘𝑖) ∈ V |
112 | 109, 110,
62, 111 | ovmpo 7326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ ω ∧ (ℎ‘𝑖) ∈ ∪ 𝐴) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖)) |
113 | 107, 108,
112 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑖 ∈ ω)
→ (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖)) |
114 | 113 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖)) |
115 | 114 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖)) |
116 | 96, 106, 115 | 3eltr3d 2847 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc (◡𝑓‘𝑧)) ∈ (𝑓‘𝑖)) |
117 | 35 | ffvelrnda 6862 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴) |
118 | 117 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴) |
119 | 118 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑓‘𝑖) ∈ 𝐴) |
120 | | eleq1 2820 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (𝑓‘𝑖) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴)) |
121 | 120 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴)) |
122 | 119, 121 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 ∈ 𝐴) |
123 | | fveq2 6675 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑧 → (◡𝑓‘𝑤) = (◡𝑓‘𝑧)) |
124 | | suceq 6238 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((◡𝑓‘𝑤) = (◡𝑓‘𝑧) → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧)) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑧 → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧)) |
126 | 125 | fveq2d 6679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑧 → (ℎ‘suc (◡𝑓‘𝑤)) = (ℎ‘suc (◡𝑓‘𝑧))) |
127 | | axcclem.3 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐺 = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) |
128 | | fvex 6688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ‘suc (◡𝑓‘𝑧)) ∈ V |
129 | 126, 127,
128 | fvmpt 6776 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝐴 → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧))) |
130 | 122, 129 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧))) |
131 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 = (𝑓‘𝑖)) |
132 | 116, 130,
131 | 3eltr4d 2848 |
. . . . . . . . . . . . . . . . . 18
⊢ (((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) ∈ 𝑧) |
133 | 132 | 3exp 1120 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ:ω⟶∪ 𝐴
∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝑧 = (𝑓‘𝑖) → (𝐺‘𝑧) ∈ 𝑧))) |
134 | 133 | com3r 87 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑓‘𝑖) → ((ℎ:ω⟶∪
𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))) |
135 | 134 | 3expd 1354 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪
𝐴 → (𝑓:ω–1-1-onto→𝐴 → (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))))) |
136 | 135 | com4r 94 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ω → (𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪
𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))))) |
137 | 136 | rexlimiv 3190 |
. . . . . . . . . . . . 13
⊢
(∃𝑖 ∈
ω 𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪
𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))) |
138 | 86, 137 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → (ℎ:ω⟶∪
𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))) |
139 | 83, 138 | mpid 44 |
. . . . . . . . . . 11
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → (ℎ:ω⟶∪
𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))) |
140 | 139 | impd 414 |
. . . . . . . . . 10
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ((ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (𝐺‘𝑧) ∈ 𝑧)) |
141 | 140 | impancom 455 |
. . . . . . . . 9
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝐴 → (𝐺‘𝑧) ∈ 𝑧)) |
142 | 82, 141 | syl5 34 |
. . . . . . . 8
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (𝐺‘𝑧) ∈ 𝑧)) |
143 | 142 | expd 419 |
. . . . . . 7
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))) |
144 | 143 | ralrimiv 3095 |
. . . . . 6
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)) |
145 | | fvrn0 6703 |
. . . . . . . . . . 11
⊢ (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) |
146 | 145 | rgenw 3065 |
. . . . . . . . . 10
⊢
∀𝑤 ∈
𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) |
147 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) |
148 | 147 | fmpt 6885 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) ↔ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅})) |
149 | 146, 148 | mpbi 233 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}) |
150 | | vex 3402 |
. . . . . . . . . . 11
⊢ ℎ ∈ V |
151 | 150 | rnex 7644 |
. . . . . . . . . 10
⊢ ran ℎ ∈ V |
152 | | p0ex 5252 |
. . . . . . . . . 10
⊢ {∅}
∈ V |
153 | 151, 152 | unex 7488 |
. . . . . . . . 9
⊢ (ran
ℎ ∪ {∅}) ∈
V |
154 | | fex2 7665 |
. . . . . . . . 9
⊢ (((𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V) |
155 | 149, 67, 153, 154 | mp3an 1462 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V |
156 | 127, 155 | eqeltri 2829 |
. . . . . . 7
⊢ 𝐺 ∈ V |
157 | | fveq1 6674 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑔‘𝑧) = (𝐺‘𝑧)) |
158 | 157 | eleq1d 2817 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝑔‘𝑧) ∈ 𝑧 ↔ (𝐺‘𝑧) ∈ 𝑧)) |
159 | 158 | imbi2d 344 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))) |
160 | 159 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))) |
161 | 156, 160 | spcev 3511 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |
162 | 144, 161 | syl 17 |
. . . . 5
⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪
𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |
163 | 76, 162 | exlimddv 1941 |
. . . 4
⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |
164 | 163 | exlimiv 1936 |
. . 3
⊢
(∃𝑓 𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |
165 | 34, 164 | sylbi 220 |
. 2
⊢ (ω
≈ 𝐴 →
∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |
166 | 32, 33, 165 | 3syl 18 |
1
⊢ (𝑥 ≈ ω →
∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧)) |