Step |
Hyp |
Ref |
Expression |
1 |
|
axcclem.1 |
⊢ 𝐴 = ( 𝑥 ∖ { ∅ } ) |
2 |
|
axcclem.2 |
⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑦 ∈ ∪ 𝐴 ↦ ( 𝑓 ‘ 𝑛 ) ) |
3 |
|
axcclem.3 |
⊢ 𝐺 = ( 𝑤 ∈ 𝐴 ↦ ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ) |
4 |
|
isfinite2 |
⊢ ( 𝐴 ≺ ω → 𝐴 ∈ Fin ) |
5 |
1
|
eleq1i |
⊢ ( 𝐴 ∈ Fin ↔ ( 𝑥 ∖ { ∅ } ) ∈ Fin ) |
6 |
|
undif1 |
⊢ ( ( 𝑥 ∖ { ∅ } ) ∪ { ∅ } ) = ( 𝑥 ∪ { ∅ } ) |
7 |
|
snfi |
⊢ { ∅ } ∈ Fin |
8 |
|
unfi |
⊢ ( ( ( 𝑥 ∖ { ∅ } ) ∈ Fin ∧ { ∅ } ∈ Fin ) → ( ( 𝑥 ∖ { ∅ } ) ∪ { ∅ } ) ∈ Fin ) |
9 |
7 8
|
mpan2 |
⊢ ( ( 𝑥 ∖ { ∅ } ) ∈ Fin → ( ( 𝑥 ∖ { ∅ } ) ∪ { ∅ } ) ∈ Fin ) |
10 |
6 9
|
eqeltrrid |
⊢ ( ( 𝑥 ∖ { ∅ } ) ∈ Fin → ( 𝑥 ∪ { ∅ } ) ∈ Fin ) |
11 |
|
ssun1 |
⊢ 𝑥 ⊆ ( 𝑥 ∪ { ∅ } ) |
12 |
|
ssfi |
⊢ ( ( ( 𝑥 ∪ { ∅ } ) ∈ Fin ∧ 𝑥 ⊆ ( 𝑥 ∪ { ∅ } ) ) → 𝑥 ∈ Fin ) |
13 |
10 11 12
|
sylancl |
⊢ ( ( 𝑥 ∖ { ∅ } ) ∈ Fin → 𝑥 ∈ Fin ) |
14 |
5 13
|
sylbi |
⊢ ( 𝐴 ∈ Fin → 𝑥 ∈ Fin ) |
15 |
|
dcomex |
⊢ ω ∈ V |
16 |
|
isfiniteg |
⊢ ( ω ∈ V → ( 𝑥 ∈ Fin ↔ 𝑥 ≺ ω ) ) |
17 |
15 16
|
ax-mp |
⊢ ( 𝑥 ∈ Fin ↔ 𝑥 ≺ ω ) |
18 |
|
sdomnen |
⊢ ( 𝑥 ≺ ω → ¬ 𝑥 ≈ ω ) |
19 |
17 18
|
sylbi |
⊢ ( 𝑥 ∈ Fin → ¬ 𝑥 ≈ ω ) |
20 |
4 14 19
|
3syl |
⊢ ( 𝐴 ≺ ω → ¬ 𝑥 ≈ ω ) |
21 |
20
|
con2i |
⊢ ( 𝑥 ≈ ω → ¬ 𝐴 ≺ ω ) |
22 |
|
sdomentr |
⊢ ( ( 𝐴 ≺ 𝑥 ∧ 𝑥 ≈ ω ) → 𝐴 ≺ ω ) |
23 |
22
|
expcom |
⊢ ( 𝑥 ≈ ω → ( 𝐴 ≺ 𝑥 → 𝐴 ≺ ω ) ) |
24 |
21 23
|
mtod |
⊢ ( 𝑥 ≈ ω → ¬ 𝐴 ≺ 𝑥 ) |
25 |
|
vex |
⊢ 𝑥 ∈ V |
26 |
|
difss |
⊢ ( 𝑥 ∖ { ∅ } ) ⊆ 𝑥 |
27 |
1 26
|
eqsstri |
⊢ 𝐴 ⊆ 𝑥 |
28 |
|
ssdomg |
⊢ ( 𝑥 ∈ V → ( 𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥 ) ) |
29 |
25 27 28
|
mp2 |
⊢ 𝐴 ≼ 𝑥 |
30 |
24 29
|
jctil |
⊢ ( 𝑥 ≈ ω → ( 𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥 ) ) |
31 |
|
bren2 |
⊢ ( 𝐴 ≈ 𝑥 ↔ ( 𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥 ) ) |
32 |
30 31
|
sylibr |
⊢ ( 𝑥 ≈ ω → 𝐴 ≈ 𝑥 ) |
33 |
|
entr |
⊢ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ≈ ω ) → 𝐴 ≈ ω ) |
34 |
32 33
|
mpancom |
⊢ ( 𝑥 ≈ ω → 𝐴 ≈ ω ) |
35 |
|
ensym |
⊢ ( 𝐴 ≈ ω → ω ≈ 𝐴 ) |
36 |
|
bren |
⊢ ( ω ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : ω –1-1-onto→ 𝐴 ) |
37 |
|
f1of |
⊢ ( 𝑓 : ω –1-1-onto→ 𝐴 → 𝑓 : ω ⟶ 𝐴 ) |
38 |
|
peano1 |
⊢ ∅ ∈ ω |
39 |
|
ffvelrn |
⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ∅ ∈ ω ) → ( 𝑓 ‘ ∅ ) ∈ 𝐴 ) |
40 |
37 38 39
|
sylancl |
⊢ ( 𝑓 : ω –1-1-onto→ 𝐴 → ( 𝑓 ‘ ∅ ) ∈ 𝐴 ) |
41 |
|
eldifn |
⊢ ( ( 𝑓 ‘ ∅ ) ∈ ( 𝑥 ∖ { ∅ } ) → ¬ ( 𝑓 ‘ ∅ ) ∈ { ∅ } ) |
42 |
41 1
|
eleq2s |
⊢ ( ( 𝑓 ‘ ∅ ) ∈ 𝐴 → ¬ ( 𝑓 ‘ ∅ ) ∈ { ∅ } ) |
43 |
|
fvex |
⊢ ( 𝑓 ‘ ∅ ) ∈ V |
44 |
43
|
elsn |
⊢ ( ( 𝑓 ‘ ∅ ) ∈ { ∅ } ↔ ( 𝑓 ‘ ∅ ) = ∅ ) |
45 |
44
|
notbii |
⊢ ( ¬ ( 𝑓 ‘ ∅ ) ∈ { ∅ } ↔ ¬ ( 𝑓 ‘ ∅ ) = ∅ ) |
46 |
|
neq0 |
⊢ ( ¬ ( 𝑓 ‘ ∅ ) = ∅ ↔ ∃ 𝑐 𝑐 ∈ ( 𝑓 ‘ ∅ ) ) |
47 |
45 46
|
bitr2i |
⊢ ( ∃ 𝑐 𝑐 ∈ ( 𝑓 ‘ ∅ ) ↔ ¬ ( 𝑓 ‘ ∅ ) ∈ { ∅ } ) |
48 |
42 47
|
sylibr |
⊢ ( ( 𝑓 ‘ ∅ ) ∈ 𝐴 → ∃ 𝑐 𝑐 ∈ ( 𝑓 ‘ ∅ ) ) |
49 |
40 48
|
syl |
⊢ ( 𝑓 : ω –1-1-onto→ 𝐴 → ∃ 𝑐 𝑐 ∈ ( 𝑓 ‘ ∅ ) ) |
50 |
|
elunii |
⊢ ( ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) ∧ ( 𝑓 ‘ ∅ ) ∈ 𝐴 ) → 𝑐 ∈ ∪ 𝐴 ) |
51 |
40 50
|
sylan2 |
⊢ ( ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) ∧ 𝑓 : ω –1-1-onto→ 𝐴 ) → 𝑐 ∈ ∪ 𝐴 ) |
52 |
37
|
ffvelrnda |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑛 ∈ ω ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ) |
53 |
|
difabs |
⊢ ( ( 𝑥 ∖ { ∅ } ) ∖ { ∅ } ) = ( 𝑥 ∖ { ∅ } ) |
54 |
1
|
difeq1i |
⊢ ( 𝐴 ∖ { ∅ } ) = ( ( 𝑥 ∖ { ∅ } ) ∖ { ∅ } ) |
55 |
53 54 1
|
3eqtr4i |
⊢ ( 𝐴 ∖ { ∅ } ) = 𝐴 |
56 |
|
pwuni |
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 |
57 |
|
ssdif |
⊢ ( 𝐴 ⊆ 𝒫 ∪ 𝐴 → ( 𝐴 ∖ { ∅ } ) ⊆ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) ) |
58 |
56 57
|
ax-mp |
⊢ ( 𝐴 ∖ { ∅ } ) ⊆ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) |
59 |
55 58
|
eqsstrri |
⊢ 𝐴 ⊆ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) |
60 |
59
|
sseli |
⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 → ( 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) ) |
61 |
60
|
ralrimivw |
⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 → ∀ 𝑦 ∈ ∪ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) ) |
62 |
52 61
|
syl |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑛 ∈ ω ) → ∀ 𝑦 ∈ ∪ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) ) |
63 |
62
|
ralrimiva |
⊢ ( 𝑓 : ω –1-1-onto→ 𝐴 → ∀ 𝑛 ∈ ω ∀ 𝑦 ∈ ∪ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) ) |
64 |
2
|
fmpo |
⊢ ( ∀ 𝑛 ∈ ω ∀ 𝑦 ∈ ∪ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) ↔ 𝐹 : ( ω × ∪ 𝐴 ) ⟶ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) ) |
65 |
63 64
|
sylib |
⊢ ( 𝑓 : ω –1-1-onto→ 𝐴 → 𝐹 : ( ω × ∪ 𝐴 ) ⟶ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) ) |
66 |
65
|
adantl |
⊢ ( ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) ∧ 𝑓 : ω –1-1-onto→ 𝐴 ) → 𝐹 : ( ω × ∪ 𝐴 ) ⟶ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) ) |
67 |
25
|
difexi |
⊢ ( 𝑥 ∖ { ∅ } ) ∈ V |
68 |
1 67
|
eqeltri |
⊢ 𝐴 ∈ V |
69 |
68
|
uniex |
⊢ ∪ 𝐴 ∈ V |
70 |
69
|
axdc4 |
⊢ ( ( 𝑐 ∈ ∪ 𝐴 ∧ 𝐹 : ( ω × ∪ 𝐴 ) ⟶ ( 𝒫 ∪ 𝐴 ∖ { ∅ } ) ) → ∃ ℎ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ( ℎ ‘ ∅ ) = 𝑐 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) |
71 |
51 66 70
|
syl2anc |
⊢ ( ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) ∧ 𝑓 : ω –1-1-onto→ 𝐴 ) → ∃ ℎ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ( ℎ ‘ ∅ ) = 𝑐 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) |
72 |
|
3simpb |
⊢ ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ ( ℎ ‘ ∅ ) = 𝑐 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) → ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) |
73 |
72
|
eximi |
⊢ ( ∃ ℎ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ( ℎ ‘ ∅ ) = 𝑐 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) → ∃ ℎ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) |
74 |
71 73
|
syl |
⊢ ( ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) ∧ 𝑓 : ω –1-1-onto→ 𝐴 ) → ∃ ℎ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) |
75 |
74
|
ex |
⊢ ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) → ( 𝑓 : ω –1-1-onto→ 𝐴 → ∃ ℎ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) ) |
76 |
75
|
exlimiv |
⊢ ( ∃ 𝑐 𝑐 ∈ ( 𝑓 ‘ ∅ ) → ( 𝑓 : ω –1-1-onto→ 𝐴 → ∃ ℎ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) ) |
77 |
49 76
|
mpcom |
⊢ ( 𝑓 : ω –1-1-onto→ 𝐴 → ∃ ℎ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) |
78 |
|
velsn |
⊢ ( 𝑧 ∈ { ∅ } ↔ 𝑧 = ∅ ) |
79 |
78
|
necon3bbii |
⊢ ( ¬ 𝑧 ∈ { ∅ } ↔ 𝑧 ≠ ∅ ) |
80 |
1
|
eleq2i |
⊢ ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ( 𝑥 ∖ { ∅ } ) ) |
81 |
|
eldif |
⊢ ( 𝑧 ∈ ( 𝑥 ∖ { ∅ } ) ↔ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ { ∅ } ) ) |
82 |
80 81
|
sylbbr |
⊢ ( ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ { ∅ } ) → 𝑧 ∈ 𝐴 ) |
83 |
79 82
|
sylan2br |
⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → 𝑧 ∈ 𝐴 ) |
84 |
|
simpl |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → 𝑓 : ω –1-1-onto→ 𝐴 ) |
85 |
|
f1ofo |
⊢ ( 𝑓 : ω –1-1-onto→ 𝐴 → 𝑓 : ω –onto→ 𝐴 ) |
86 |
|
foelrn |
⊢ ( ( 𝑓 : ω –onto→ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑖 ∈ ω 𝑧 = ( 𝑓 ‘ 𝑖 ) ) |
87 |
85 86
|
sylan |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑖 ∈ ω 𝑧 = ( 𝑓 ‘ 𝑖 ) ) |
88 |
|
suceq |
⊢ ( 𝑘 = 𝑖 → suc 𝑘 = suc 𝑖 ) |
89 |
88
|
fveq2d |
⊢ ( 𝑘 = 𝑖 → ( ℎ ‘ suc 𝑘 ) = ( ℎ ‘ suc 𝑖 ) ) |
90 |
|
id |
⊢ ( 𝑘 = 𝑖 → 𝑘 = 𝑖 ) |
91 |
|
fveq2 |
⊢ ( 𝑘 = 𝑖 → ( ℎ ‘ 𝑘 ) = ( ℎ ‘ 𝑖 ) ) |
92 |
90 91
|
oveq12d |
⊢ ( 𝑘 = 𝑖 → ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) = ( 𝑖 𝐹 ( ℎ ‘ 𝑖 ) ) ) |
93 |
89 92
|
eleq12d |
⊢ ( 𝑘 = 𝑖 → ( ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ↔ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝑖 𝐹 ( ℎ ‘ 𝑖 ) ) ) ) |
94 |
93
|
rspcv |
⊢ ( 𝑖 ∈ ω → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) → ( ℎ ‘ suc 𝑖 ) ∈ ( 𝑖 𝐹 ( ℎ ‘ 𝑖 ) ) ) ) |
95 |
94
|
3ad2ant3 |
⊢ ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) → ( ℎ ‘ suc 𝑖 ) ∈ ( 𝑖 𝐹 ( ℎ ‘ 𝑖 ) ) ) ) |
96 |
95
|
imp |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) → ( ℎ ‘ suc 𝑖 ) ∈ ( 𝑖 𝐹 ( ℎ ‘ 𝑖 ) ) ) |
97 |
96
|
3adant3 |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → ( ℎ ‘ suc 𝑖 ) ∈ ( 𝑖 𝐹 ( ℎ ‘ 𝑖 ) ) ) |
98 |
|
eqcom |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑖 ) ↔ ( 𝑓 ‘ 𝑖 ) = 𝑧 ) |
99 |
|
f1ocnvfv |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) → ( ( 𝑓 ‘ 𝑖 ) = 𝑧 → ( ◡ 𝑓 ‘ 𝑧 ) = 𝑖 ) ) |
100 |
98 99
|
syl5bi |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) → ( 𝑧 = ( 𝑓 ‘ 𝑖 ) → ( ◡ 𝑓 ‘ 𝑧 ) = 𝑖 ) ) |
101 |
100
|
3adant1 |
⊢ ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) → ( 𝑧 = ( 𝑓 ‘ 𝑖 ) → ( ◡ 𝑓 ‘ 𝑧 ) = 𝑖 ) ) |
102 |
101
|
imp |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → ( ◡ 𝑓 ‘ 𝑧 ) = 𝑖 ) |
103 |
102
|
eqcomd |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → 𝑖 = ( ◡ 𝑓 ‘ 𝑧 ) ) |
104 |
103
|
3adant2 |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → 𝑖 = ( ◡ 𝑓 ‘ 𝑧 ) ) |
105 |
|
suceq |
⊢ ( 𝑖 = ( ◡ 𝑓 ‘ 𝑧 ) → suc 𝑖 = suc ( ◡ 𝑓 ‘ 𝑧 ) ) |
106 |
104 105
|
syl |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → suc 𝑖 = suc ( ◡ 𝑓 ‘ 𝑧 ) ) |
107 |
106
|
fveq2d |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → ( ℎ ‘ suc 𝑖 ) = ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑧 ) ) ) |
108 |
|
simpr |
⊢ ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑖 ∈ ω ) → 𝑖 ∈ ω ) |
109 |
|
ffvelrn |
⊢ ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑖 ∈ ω ) → ( ℎ ‘ 𝑖 ) ∈ ∪ 𝐴 ) |
110 |
|
fveq2 |
⊢ ( 𝑛 = 𝑖 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑖 ) ) |
111 |
|
eqidd |
⊢ ( 𝑦 = ( ℎ ‘ 𝑖 ) → ( 𝑓 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ) |
112 |
|
fvex |
⊢ ( 𝑓 ‘ 𝑖 ) ∈ V |
113 |
110 111 2 112
|
ovmpo |
⊢ ( ( 𝑖 ∈ ω ∧ ( ℎ ‘ 𝑖 ) ∈ ∪ 𝐴 ) → ( 𝑖 𝐹 ( ℎ ‘ 𝑖 ) ) = ( 𝑓 ‘ 𝑖 ) ) |
114 |
108 109 113
|
syl2anc |
⊢ ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑖 ∈ ω ) → ( 𝑖 𝐹 ( ℎ ‘ 𝑖 ) ) = ( 𝑓 ‘ 𝑖 ) ) |
115 |
114
|
3adant2 |
⊢ ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) → ( 𝑖 𝐹 ( ℎ ‘ 𝑖 ) ) = ( 𝑓 ‘ 𝑖 ) ) |
116 |
115
|
3ad2ant1 |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → ( 𝑖 𝐹 ( ℎ ‘ 𝑖 ) ) = ( 𝑓 ‘ 𝑖 ) ) |
117 |
97 107 116
|
3eltr3d |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑓 ‘ 𝑖 ) ) |
118 |
37
|
ffvelrnda |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) → ( 𝑓 ‘ 𝑖 ) ∈ 𝐴 ) |
119 |
118
|
3adant1 |
⊢ ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) → ( 𝑓 ‘ 𝑖 ) ∈ 𝐴 ) |
120 |
119
|
3ad2ant1 |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → ( 𝑓 ‘ 𝑖 ) ∈ 𝐴 ) |
121 |
|
eleq1 |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑖 ) → ( 𝑧 ∈ 𝐴 ↔ ( 𝑓 ‘ 𝑖 ) ∈ 𝐴 ) ) |
122 |
121
|
3ad2ant3 |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → ( 𝑧 ∈ 𝐴 ↔ ( 𝑓 ‘ 𝑖 ) ∈ 𝐴 ) ) |
123 |
120 122
|
mpbird |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → 𝑧 ∈ 𝐴 ) |
124 |
|
fveq2 |
⊢ ( 𝑤 = 𝑧 → ( ◡ 𝑓 ‘ 𝑤 ) = ( ◡ 𝑓 ‘ 𝑧 ) ) |
125 |
|
suceq |
⊢ ( ( ◡ 𝑓 ‘ 𝑤 ) = ( ◡ 𝑓 ‘ 𝑧 ) → suc ( ◡ 𝑓 ‘ 𝑤 ) = suc ( ◡ 𝑓 ‘ 𝑧 ) ) |
126 |
124 125
|
syl |
⊢ ( 𝑤 = 𝑧 → suc ( ◡ 𝑓 ‘ 𝑤 ) = suc ( ◡ 𝑓 ‘ 𝑧 ) ) |
127 |
126
|
fveq2d |
⊢ ( 𝑤 = 𝑧 → ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) = ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑧 ) ) ) |
128 |
|
fvex |
⊢ ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑧 ) ) ∈ V |
129 |
127 3 128
|
fvmpt |
⊢ ( 𝑧 ∈ 𝐴 → ( 𝐺 ‘ 𝑧 ) = ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑧 ) ) ) |
130 |
123 129
|
syl |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → ( 𝐺 ‘ 𝑧 ) = ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑧 ) ) ) |
131 |
|
simp3 |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → 𝑧 = ( 𝑓 ‘ 𝑖 ) ) |
132 |
117 130 131
|
3eltr4d |
⊢ ( ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ∧ 𝑧 = ( 𝑓 ‘ 𝑖 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) |
133 |
132
|
3exp |
⊢ ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) → ( 𝑧 = ( 𝑓 ‘ 𝑖 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
134 |
133
|
com3r |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑖 ) → ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑖 ∈ ω ) → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
135 |
134
|
3expd |
⊢ ( 𝑧 = ( 𝑓 ‘ 𝑖 ) → ( ℎ : ω ⟶ ∪ 𝐴 → ( 𝑓 : ω –1-1-onto→ 𝐴 → ( 𝑖 ∈ ω → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) ) ) ) |
136 |
135
|
com4r |
⊢ ( 𝑖 ∈ ω → ( 𝑧 = ( 𝑓 ‘ 𝑖 ) → ( ℎ : ω ⟶ ∪ 𝐴 → ( 𝑓 : ω –1-1-onto→ 𝐴 → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) ) ) ) |
137 |
136
|
rexlimiv |
⊢ ( ∃ 𝑖 ∈ ω 𝑧 = ( 𝑓 ‘ 𝑖 ) → ( ℎ : ω ⟶ ∪ 𝐴 → ( 𝑓 : ω –1-1-onto→ 𝐴 → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) ) ) |
138 |
87 137
|
syl |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ℎ : ω ⟶ ∪ 𝐴 → ( 𝑓 : ω –1-1-onto→ 𝐴 → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) ) ) |
139 |
84 138
|
mpid |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ℎ : ω ⟶ ∪ 𝐴 → ( ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
140 |
139
|
impd |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) |
141 |
140
|
impancom |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) → ( 𝑧 ∈ 𝐴 → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) |
142 |
83 141
|
syl5 |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) |
143 |
142
|
expd |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) → ( 𝑧 ∈ 𝑥 → ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
144 |
143
|
ralrimiv |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) |
145 |
|
fvrn0 |
⊢ ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ∈ ( ran ℎ ∪ { ∅ } ) |
146 |
145
|
rgenw |
⊢ ∀ 𝑤 ∈ 𝐴 ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ∈ ( ran ℎ ∪ { ∅ } ) |
147 |
|
eqid |
⊢ ( 𝑤 ∈ 𝐴 ↦ ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ) |
148 |
147
|
fmpt |
⊢ ( ∀ 𝑤 ∈ 𝐴 ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ∈ ( ran ℎ ∪ { ∅ } ) ↔ ( 𝑤 ∈ 𝐴 ↦ ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ) : 𝐴 ⟶ ( ran ℎ ∪ { ∅ } ) ) |
149 |
146 148
|
mpbi |
⊢ ( 𝑤 ∈ 𝐴 ↦ ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ) : 𝐴 ⟶ ( ran ℎ ∪ { ∅ } ) |
150 |
|
vex |
⊢ ℎ ∈ V |
151 |
150
|
rnex |
⊢ ran ℎ ∈ V |
152 |
|
p0ex |
⊢ { ∅ } ∈ V |
153 |
151 152
|
unex |
⊢ ( ran ℎ ∪ { ∅ } ) ∈ V |
154 |
|
fex2 |
⊢ ( ( ( 𝑤 ∈ 𝐴 ↦ ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ) : 𝐴 ⟶ ( ran ℎ ∪ { ∅ } ) ∧ 𝐴 ∈ V ∧ ( ran ℎ ∪ { ∅ } ) ∈ V ) → ( 𝑤 ∈ 𝐴 ↦ ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ) ∈ V ) |
155 |
149 68 153 154
|
mp3an |
⊢ ( 𝑤 ∈ 𝐴 ↦ ( ℎ ‘ suc ( ◡ 𝑓 ‘ 𝑤 ) ) ) ∈ V |
156 |
3 155
|
eqeltri |
⊢ 𝐺 ∈ V |
157 |
|
fveq1 |
⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) |
158 |
157
|
eleq1d |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) |
159 |
158
|
imbi2d |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
160 |
159
|
ralbidv |
⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
161 |
156 160
|
spcev |
⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑔 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) |
162 |
144 161
|
syl |
⊢ ( ( 𝑓 : ω –1-1-onto→ 𝐴 ∧ ( ℎ : ω ⟶ ∪ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( ℎ ‘ 𝑘 ) ) ) ) → ∃ 𝑔 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) |
163 |
77 162
|
exlimddv |
⊢ ( 𝑓 : ω –1-1-onto→ 𝐴 → ∃ 𝑔 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) |
164 |
163
|
exlimiv |
⊢ ( ∃ 𝑓 𝑓 : ω –1-1-onto→ 𝐴 → ∃ 𝑔 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) |
165 |
36 164
|
sylbi |
⊢ ( ω ≈ 𝐴 → ∃ 𝑔 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) |
166 |
34 35 165
|
3syl |
⊢ ( 𝑥 ≈ ω → ∃ 𝑔 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) ) |