Step |
Hyp |
Ref |
Expression |
1 |
|
axcc2lem.1 |
⊢ 𝐾 = ( 𝑛 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ) |
2 |
|
axcc2lem.2 |
⊢ 𝐴 = ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) |
3 |
|
axcc2lem.3 |
⊢ 𝐺 = ( 𝑛 ∈ ω ↦ ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) |
4 |
|
fvex |
⊢ ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ∈ V |
5 |
4 3
|
fnmpti |
⊢ 𝐺 Fn ω |
6 |
|
snex |
⊢ { 𝑛 } ∈ V |
7 |
|
fvex |
⊢ ( 𝐾 ‘ 𝑛 ) ∈ V |
8 |
6 7
|
xpex |
⊢ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ∈ V |
9 |
2
|
fvmpt2 |
⊢ ( ( 𝑛 ∈ ω ∧ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ∈ V ) → ( 𝐴 ‘ 𝑛 ) = ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) |
10 |
8 9
|
mpan2 |
⊢ ( 𝑛 ∈ ω → ( 𝐴 ‘ 𝑛 ) = ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) |
11 |
|
vex |
⊢ 𝑛 ∈ V |
12 |
11
|
snnz |
⊢ { 𝑛 } ≠ ∅ |
13 |
|
0ex |
⊢ ∅ ∈ V |
14 |
13
|
snnz |
⊢ { ∅ } ≠ ∅ |
15 |
|
iftrue |
⊢ ( ( 𝐹 ‘ 𝑛 ) = ∅ → if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) = { ∅ } ) |
16 |
15
|
neeq1d |
⊢ ( ( 𝐹 ‘ 𝑛 ) = ∅ → ( if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ≠ ∅ ↔ { ∅ } ≠ ∅ ) ) |
17 |
14 16
|
mpbiri |
⊢ ( ( 𝐹 ‘ 𝑛 ) = ∅ → if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ≠ ∅ ) |
18 |
|
iffalse |
⊢ ( ¬ ( 𝐹 ‘ 𝑛 ) = ∅ → if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) = ( 𝐹 ‘ 𝑛 ) ) |
19 |
|
neqne |
⊢ ( ¬ ( 𝐹 ‘ 𝑛 ) = ∅ → ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) |
20 |
18 19
|
eqnetrd |
⊢ ( ¬ ( 𝐹 ‘ 𝑛 ) = ∅ → if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ≠ ∅ ) |
21 |
17 20
|
pm2.61i |
⊢ if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ≠ ∅ |
22 |
|
p0ex |
⊢ { ∅ } ∈ V |
23 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑛 ) ∈ V |
24 |
22 23
|
ifex |
⊢ if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ∈ V |
25 |
1
|
fvmpt2 |
⊢ ( ( 𝑛 ∈ ω ∧ if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ∈ V ) → ( 𝐾 ‘ 𝑛 ) = if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ) |
26 |
24 25
|
mpan2 |
⊢ ( 𝑛 ∈ ω → ( 𝐾 ‘ 𝑛 ) = if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ) |
27 |
26
|
neeq1d |
⊢ ( 𝑛 ∈ ω → ( ( 𝐾 ‘ 𝑛 ) ≠ ∅ ↔ if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ≠ ∅ ) ) |
28 |
21 27
|
mpbiri |
⊢ ( 𝑛 ∈ ω → ( 𝐾 ‘ 𝑛 ) ≠ ∅ ) |
29 |
|
xpnz |
⊢ ( ( { 𝑛 } ≠ ∅ ∧ ( 𝐾 ‘ 𝑛 ) ≠ ∅ ) ↔ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ≠ ∅ ) |
30 |
29
|
biimpi |
⊢ ( ( { 𝑛 } ≠ ∅ ∧ ( 𝐾 ‘ 𝑛 ) ≠ ∅ ) → ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ≠ ∅ ) |
31 |
12 28 30
|
sylancr |
⊢ ( 𝑛 ∈ ω → ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ≠ ∅ ) |
32 |
10 31
|
eqnetrd |
⊢ ( 𝑛 ∈ ω → ( 𝐴 ‘ 𝑛 ) ≠ ∅ ) |
33 |
8 2
|
fnmpti |
⊢ 𝐴 Fn ω |
34 |
|
fnfvelrn |
⊢ ( ( 𝐴 Fn ω ∧ 𝑛 ∈ ω ) → ( 𝐴 ‘ 𝑛 ) ∈ ran 𝐴 ) |
35 |
33 34
|
mpan |
⊢ ( 𝑛 ∈ ω → ( 𝐴 ‘ 𝑛 ) ∈ ran 𝐴 ) |
36 |
|
neeq1 |
⊢ ( 𝑧 = ( 𝐴 ‘ 𝑛 ) → ( 𝑧 ≠ ∅ ↔ ( 𝐴 ‘ 𝑛 ) ≠ ∅ ) ) |
37 |
|
fveq2 |
⊢ ( 𝑧 = ( 𝐴 ‘ 𝑛 ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) |
38 |
|
id |
⊢ ( 𝑧 = ( 𝐴 ‘ 𝑛 ) → 𝑧 = ( 𝐴 ‘ 𝑛 ) ) |
39 |
37 38
|
eleq12d |
⊢ ( 𝑧 = ( 𝐴 ‘ 𝑛 ) → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 𝐴 ‘ 𝑛 ) ) ) |
40 |
36 39
|
imbi12d |
⊢ ( 𝑧 = ( 𝐴 ‘ 𝑛 ) → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( ( 𝐴 ‘ 𝑛 ) ≠ ∅ → ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 𝐴 ‘ 𝑛 ) ) ) ) |
41 |
40
|
rspccv |
⊢ ( ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( 𝐴 ‘ 𝑛 ) ∈ ran 𝐴 → ( ( 𝐴 ‘ 𝑛 ) ≠ ∅ → ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 𝐴 ‘ 𝑛 ) ) ) ) |
42 |
35 41
|
syl5 |
⊢ ( ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑛 ∈ ω → ( ( 𝐴 ‘ 𝑛 ) ≠ ∅ → ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 𝐴 ‘ 𝑛 ) ) ) ) |
43 |
32 42
|
mpdi |
⊢ ( ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑛 ∈ ω → ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 𝐴 ‘ 𝑛 ) ) ) |
44 |
43
|
impcom |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 𝐴 ‘ 𝑛 ) ) |
45 |
10
|
eleq2d |
⊢ ( 𝑛 ∈ ω → ( ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 𝐴 ‘ 𝑛 ) ↔ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) ) |
46 |
45
|
adantr |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( 𝐴 ‘ 𝑛 ) ↔ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) ) |
47 |
44 46
|
mpbid |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) |
48 |
|
xp2nd |
⊢ ( ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) → ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ∈ ( 𝐾 ‘ 𝑛 ) ) |
49 |
47 48
|
syl |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ∈ ( 𝐾 ‘ 𝑛 ) ) |
50 |
49
|
3adant3 |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) → ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ∈ ( 𝐾 ‘ 𝑛 ) ) |
51 |
3
|
fvmpt2 |
⊢ ( ( 𝑛 ∈ ω ∧ ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ∈ V ) → ( 𝐺 ‘ 𝑛 ) = ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) |
52 |
4 51
|
mpan2 |
⊢ ( 𝑛 ∈ ω → ( 𝐺 ‘ 𝑛 ) = ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) |
53 |
52
|
3ad2ant1 |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) → ( 𝐺 ‘ 𝑛 ) = ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) |
54 |
53
|
eqcomd |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) → ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝐺 ‘ 𝑛 ) ) |
55 |
26
|
3ad2ant1 |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) → ( 𝐾 ‘ 𝑛 ) = if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) ) |
56 |
|
ifnefalse |
⊢ ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) = ( 𝐹 ‘ 𝑛 ) ) |
57 |
56
|
3ad2ant3 |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) → if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) = ( 𝐹 ‘ 𝑛 ) ) |
58 |
55 57
|
eqtrd |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) → ( 𝐾 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) ) |
59 |
50 54 58
|
3eltr3d |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) → ( 𝐺 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) |
60 |
59
|
3expia |
⊢ ( ( 𝑛 ∈ ω ∧ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝐺 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) |
61 |
60
|
expcom |
⊢ ( ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑛 ∈ ω → ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝐺 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) ) |
62 |
61
|
ralrimiv |
⊢ ( ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝐺 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) |
63 |
|
omex |
⊢ ω ∈ V |
64 |
|
fnex |
⊢ ( ( 𝐺 Fn ω ∧ ω ∈ V ) → 𝐺 ∈ V ) |
65 |
5 63 64
|
mp2an |
⊢ 𝐺 ∈ V |
66 |
|
fneq1 |
⊢ ( 𝑔 = 𝐺 → ( 𝑔 Fn ω ↔ 𝐺 Fn ω ) ) |
67 |
|
fveq1 |
⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) ) |
68 |
67
|
eleq1d |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝐺 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) |
69 |
68
|
imbi2d |
⊢ ( 𝑔 = 𝐺 → ( ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝐺 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) ) |
70 |
69
|
ralbidv |
⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ↔ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝐺 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) ) |
71 |
66 70
|
anbi12d |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝐺 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝐺 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
72 |
65 71
|
spcev |
⊢ ( ( 𝐺 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝐺 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ∃ 𝑔 ( 𝑔 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) ) |
73 |
5 62 72
|
sylancr |
⊢ ( ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑔 ( 𝑔 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) ) |
74 |
8
|
a1i |
⊢ ( ( ω ∈ V ∧ 𝑛 ∈ ω ) → ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ∈ V ) |
75 |
74 2
|
fmptd |
⊢ ( ω ∈ V → 𝐴 : ω ⟶ V ) |
76 |
63 75
|
ax-mp |
⊢ 𝐴 : ω ⟶ V |
77 |
|
sneq |
⊢ ( 𝑛 = 𝑘 → { 𝑛 } = { 𝑘 } ) |
78 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑘 ) ) |
79 |
77 78
|
xpeq12d |
⊢ ( 𝑛 = 𝑘 → ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) ) |
80 |
79 2 8
|
fvmpt3i |
⊢ ( 𝑘 ∈ ω → ( 𝐴 ‘ 𝑘 ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) ) |
81 |
80
|
adantl |
⊢ ( ( 𝑛 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝐴 ‘ 𝑘 ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) ) |
82 |
81
|
eqeq2d |
⊢ ( ( 𝑛 ∈ ω ∧ 𝑘 ∈ ω ) → ( ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) ↔ ( 𝐴 ‘ 𝑛 ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) ) ) |
83 |
10
|
adantr |
⊢ ( ( 𝑛 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝐴 ‘ 𝑛 ) = ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) |
84 |
83
|
eqeq1d |
⊢ ( ( 𝑛 ∈ ω ∧ 𝑘 ∈ ω ) → ( ( 𝐴 ‘ 𝑛 ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) ↔ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) ) ) |
85 |
|
xp11 |
⊢ ( ( { 𝑛 } ≠ ∅ ∧ ( 𝐾 ‘ 𝑛 ) ≠ ∅ ) → ( ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) ↔ ( { 𝑛 } = { 𝑘 } ∧ ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑘 ) ) ) ) |
86 |
12 28 85
|
sylancr |
⊢ ( 𝑛 ∈ ω → ( ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) ↔ ( { 𝑛 } = { 𝑘 } ∧ ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑘 ) ) ) ) |
87 |
11
|
sneqr |
⊢ ( { 𝑛 } = { 𝑘 } → 𝑛 = 𝑘 ) |
88 |
87
|
adantr |
⊢ ( ( { 𝑛 } = { 𝑘 } ∧ ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑘 ) ) → 𝑛 = 𝑘 ) |
89 |
86 88
|
syl6bi |
⊢ ( 𝑛 ∈ ω → ( ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) → 𝑛 = 𝑘 ) ) |
90 |
89
|
adantr |
⊢ ( ( 𝑛 ∈ ω ∧ 𝑘 ∈ ω ) → ( ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) → 𝑛 = 𝑘 ) ) |
91 |
84 90
|
sylbid |
⊢ ( ( 𝑛 ∈ ω ∧ 𝑘 ∈ ω ) → ( ( 𝐴 ‘ 𝑛 ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) → 𝑛 = 𝑘 ) ) |
92 |
82 91
|
sylbid |
⊢ ( ( 𝑛 ∈ ω ∧ 𝑘 ∈ ω ) → ( ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) → 𝑛 = 𝑘 ) ) |
93 |
92
|
rgen2 |
⊢ ∀ 𝑛 ∈ ω ∀ 𝑘 ∈ ω ( ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) → 𝑛 = 𝑘 ) |
94 |
|
dff13 |
⊢ ( 𝐴 : ω –1-1→ V ↔ ( 𝐴 : ω ⟶ V ∧ ∀ 𝑛 ∈ ω ∀ 𝑘 ∈ ω ( ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) → 𝑛 = 𝑘 ) ) ) |
95 |
76 93 94
|
mpbir2an |
⊢ 𝐴 : ω –1-1→ V |
96 |
|
f1f1orn |
⊢ ( 𝐴 : ω –1-1→ V → 𝐴 : ω –1-1-onto→ ran 𝐴 ) |
97 |
63
|
f1oen |
⊢ ( 𝐴 : ω –1-1-onto→ ran 𝐴 → ω ≈ ran 𝐴 ) |
98 |
|
ensym |
⊢ ( ω ≈ ran 𝐴 → ran 𝐴 ≈ ω ) |
99 |
96 97 98
|
3syl |
⊢ ( 𝐴 : ω –1-1→ V → ran 𝐴 ≈ ω ) |
100 |
2
|
rneqi |
⊢ ran 𝐴 = ran ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) |
101 |
|
dmmptg |
⊢ ( ∀ 𝑛 ∈ ω ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ∈ V → dom ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) = ω ) |
102 |
8
|
a1i |
⊢ ( 𝑛 ∈ ω → ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ∈ V ) |
103 |
101 102
|
mprg |
⊢ dom ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) = ω |
104 |
103 63
|
eqeltri |
⊢ dom ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) ∈ V |
105 |
|
funmpt |
⊢ Fun ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) |
106 |
|
funrnex |
⊢ ( dom ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) ∈ V → ( Fun ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) → ran ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) ∈ V ) ) |
107 |
104 105 106
|
mp2 |
⊢ ran ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) ) ∈ V |
108 |
100 107
|
eqeltri |
⊢ ran 𝐴 ∈ V |
109 |
|
breq1 |
⊢ ( 𝑎 = ran 𝐴 → ( 𝑎 ≈ ω ↔ ran 𝐴 ≈ ω ) ) |
110 |
|
raleq |
⊢ ( 𝑎 = ran 𝐴 → ( ∀ 𝑧 ∈ 𝑎 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
111 |
110
|
exbidv |
⊢ ( 𝑎 = ran 𝐴 → ( ∃ 𝑓 ∀ 𝑧 ∈ 𝑎 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∃ 𝑓 ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ) |
112 |
109 111
|
imbi12d |
⊢ ( 𝑎 = ran 𝐴 → ( ( 𝑎 ≈ ω → ∃ 𝑓 ∀ 𝑧 ∈ 𝑎 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ↔ ( ran 𝐴 ≈ ω → ∃ 𝑓 ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ) ) |
113 |
|
ax-cc |
⊢ ( 𝑎 ≈ ω → ∃ 𝑓 ∀ 𝑧 ∈ 𝑎 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
114 |
108 112 113
|
vtocl |
⊢ ( ran 𝐴 ≈ ω → ∃ 𝑓 ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) |
115 |
95 99 114
|
mp2b |
⊢ ∃ 𝑓 ∀ 𝑧 ∈ ran 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) |
116 |
73 115
|
exlimiiv |
⊢ ∃ 𝑔 ( 𝑔 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) ) |