Metamath Proof Explorer

Theorem axcc2lem

Description: Lemma for axcc2 . (Contributed by Mario Carneiro, 8-Feb-2013)

Ref Expression
Hypotheses axcc2lem.1 ⊢ 𝐾 = ( 𝑛 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) )
axcc2lem.2 ⊢ 𝐴 = ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) )
axcc2lem.3 ⊢ 𝐺 = ( 𝑛 ∈ ω ↦ ( 2nd ‘ ( 𝑓 ‘ ( 𝐴 ‘ 𝑛 ) ) ) )
Assertion axcc2lem ∃ 𝑔 ( 𝑔 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) )

Proof

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 vsnex ⊢ { 𝑛 } ∈ 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 biimtrdi ⊢ ( 𝑛 ∈ ω → ( ( { 𝑛 } × ( 𝐾 ‘ 𝑛 ) ) = ( { 𝑘 } × ( 𝐾 ‘ 𝑘 ) ) → 𝑛 = 𝑘 ) )
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 ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) )