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 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 ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹𝑛 ) ≠ ∅ → ( 𝑔𝑛 ) ∈ ( 𝐹𝑛 ) ) )