Metamath Proof Explorer

Theorem axdc2lem

Description: Lemma for axdc2 . We construct a relation R based on F such that x R y iff y e. ( Fx ) , and show that the "function" described by ax-dc can be restricted so that it is a real function (since the stated properties only show that it is the superset of a function). (Contributed by Mario Carneiro, 25-Jan-2013) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses axdc2lem.1 ⊢ 𝐴 ∈ V
axdc2lem.2 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
axdc2lem.3 ⊢ 𝐺 = ( 𝑥 ∈ ω ↦ ( ℎ ‘ 𝑥 ) )
Assertion axdc2lem ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc2lem.1 ⊢ 𝐴 ∈ V
2 axdc2lem.2 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
3 axdc2lem.3 ⊢ 𝐺 = ( 𝑥 ∈ ω ↦ ( ℎ ‘ 𝑥 ) )
4 2 dmeqi ⊢ dom 𝑅 = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
5 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
6 5 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
7 dmopab ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
8 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
9 6 7 8 3eqtr4i ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) }
10 4 9 eqtri ⊢ dom 𝑅 = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) }
11 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
12 eldifsni ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
13 n0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) )
14 12 13 sylib ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) )
15 11 14 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) )
16 15 ralrimiva ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) )
17 rabid2 ⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) )
18 16 17 sylibr ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → 𝐴 = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } )
19 10 18 eqtr4id ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → dom 𝑅 = 𝐴 )
20 19 neeq1d ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅ ) )
21 20 biimparc ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → dom 𝑅 ≠ ∅ )
22 2 rneqi ⊢ ran 𝑅 = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
23 rnopab ⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
24 22 23 eqtri ⊢ ran 𝑅 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
25 eldifi ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝒫 𝐴 )
26 elelpwi ⊢ ( ( 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝒫 𝐴 ) → 𝑦 ∈ 𝐴 )
27 26 expcom ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝒫 𝐴 → ( 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐴 ) )
28 11 25 27 3syl ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ 𝐴 ) )
29 28 expimpd ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑦 ∈ 𝐴 ) )
30 29 exlimdv ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑦 ∈ 𝐴 ) )
31 30 abssdv ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ⊆ 𝐴 )
32 24 31 eqsstrid ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ran 𝑅 ⊆ 𝐴 )
33 32 19 sseqtrrd ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ran 𝑅 ⊆ dom 𝑅 )
34 33 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ran 𝑅 ⊆ dom 𝑅 )
35 fvrn0 ⊢ ( 𝐹 ‘ 𝑥 ) ∈ ( ran 𝐹 ∪ { ∅ } )
36 elssuni ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ran 𝐹 ∪ { ∅ } ) → ( 𝐹 ‘ 𝑥 ) ⊆ ∪ ( ran 𝐹 ∪ { ∅ } ) )
37 35 36 ax-mp ⊢ ( 𝐹 ‘ 𝑥 ) ⊆ ∪ ( ran 𝐹 ∪ { ∅ } )
38 37 sseli ⊢ ( 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ ∪ ( ran 𝐹 ∪ { ∅ } ) )
39 38 anim2i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ ( ran 𝐹 ∪ { ∅ } ) ) )
40 39 ssopab2i ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ ( ran 𝐹 ∪ { ∅ } ) ) }
41 df-xp ⊢ ( 𝐴 × ∪ ( ran 𝐹 ∪ { ∅ } ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ ( ran 𝐹 ∪ { ∅ } ) ) }
42 40 2 41 3sstr4i ⊢ 𝑅 ⊆ ( 𝐴 × ∪ ( ran 𝐹 ∪ { ∅ } ) )
43 frn ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ran 𝐹 ⊆ ( 𝒫 𝐴 ∖ { ∅ } ) )
44 43 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ran 𝐹 ⊆ ( 𝒫 𝐴 ∖ { ∅ } ) )
45 1 pwex ⊢ 𝒫 𝐴 ∈ V
46 45 difexi ⊢ ( 𝒫 𝐴 ∖ { ∅ } ) ∈ V
47 46 ssex ⊢ ( ran 𝐹 ⊆ ( 𝒫 𝐴 ∖ { ∅ } ) → ran 𝐹 ∈ V )
48 44 47 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ran 𝐹 ∈ V )
49 p0ex ⊢ { ∅ } ∈ V
50 unexg ⊢ ( ( ran 𝐹 ∈ V ∧ { ∅ } ∈ V ) → ( ran 𝐹 ∪ { ∅ } ) ∈ V )
51 48 49 50 sylancl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ran 𝐹 ∪ { ∅ } ) ∈ V )
52 51 uniexd ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∪ ( ran 𝐹 ∪ { ∅ } ) ∈ V )
53 xpexg ⊢ ( ( 𝐴 ∈ V ∧ ∪ ( ran 𝐹 ∪ { ∅ } ) ∈ V ) → ( 𝐴 × ∪ ( ran 𝐹 ∪ { ∅ } ) ) ∈ V )
54 1 52 53 sylancr ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( 𝐴 × ∪ ( ran 𝐹 ∪ { ∅ } ) ) ∈ V )
55 ssexg ⊢ ( ( 𝑅 ⊆ ( 𝐴 × ∪ ( ran 𝐹 ∪ { ∅ } ) ) ∧ ( 𝐴 × ∪ ( ran 𝐹 ∪ { ∅ } ) ) ∈ V ) → 𝑅 ∈ V )
56 42 54 55 sylancr ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → 𝑅 ∈ V )
57 n0 ⊢ ( dom 𝑟 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ dom 𝑟 )
58 vex ⊢ 𝑥 ∈ V
59 58 eldm ⊢ ( 𝑥 ∈ dom 𝑟 ↔ ∃ 𝑦 𝑥 𝑟 𝑦 )
60 59 exbii ⊢ ( ∃ 𝑥 𝑥 ∈ dom 𝑟 ↔ ∃ 𝑥 ∃ 𝑦 𝑥 𝑟 𝑦 )
61 57 60 bitr2i ⊢ ( ∃ 𝑥 ∃ 𝑦 𝑥 𝑟 𝑦 ↔ dom 𝑟 ≠ ∅ )
62 dmeq ⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
63 62 neeq1d ⊢ ( 𝑟 = 𝑅 → ( dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅ ) )
64 61 63 bitrid ⊢ ( 𝑟 = 𝑅 → ( ∃ 𝑥 ∃ 𝑦 𝑥 𝑟 𝑦 ↔ dom 𝑅 ≠ ∅ ) )
65 rneq ⊢ ( 𝑟 = 𝑅 → ran 𝑟 = ran 𝑅 )
66 65 62 sseq12d ⊢ ( 𝑟 = 𝑅 → ( ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅 ) )
67 64 66 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ∃ 𝑥 ∃ 𝑦 𝑥 𝑟 𝑦 ∧ ran 𝑟 ⊆ dom 𝑟 ) ↔ ( dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅 ) ) )
68 breq ⊢ ( 𝑟 = 𝑅 → ( ( ℎ ‘ 𝑘 ) 𝑟 ( ℎ ‘ suc 𝑘 ) ↔ ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) )
69 68 ralbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑟 ( ℎ ‘ suc 𝑘 ) ↔ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) )
70 69 exbidv ⊢ ( 𝑟 = 𝑅 → ( ∃ ℎ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑟 ( ℎ ‘ suc 𝑘 ) ↔ ∃ ℎ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) )
71 67 70 imbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( ∃ 𝑥 ∃ 𝑦 𝑥 𝑟 𝑦 ∧ ran 𝑟 ⊆ dom 𝑟 ) → ∃ ℎ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑟 ( ℎ ‘ suc 𝑘 ) ) ↔ ( ( dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅 ) → ∃ ℎ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) ) )
72 ax-dc ⊢ ( ( ∃ 𝑥 ∃ 𝑦 𝑥 𝑟 𝑦 ∧ ran 𝑟 ⊆ dom 𝑟 ) → ∃ ℎ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑟 ( ℎ ‘ suc 𝑘 ) )
73 71 72 vtoclg ⊢ ( 𝑅 ∈ V → ( ( dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅 ) → ∃ ℎ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) )
74 56 73 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ( ( dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅 ) → ∃ ℎ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) )
75 21 34 74 mp2and ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ ℎ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) )
76 simpr ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) )
77 fveq2 ⊢ ( 𝑘 = 𝑥 → ( ℎ ‘ 𝑘 ) = ( ℎ ‘ 𝑥 ) )
78 suceq ⊢ ( 𝑘 = 𝑥 → suc 𝑘 = suc 𝑥 )
79 78 fveq2d ⊢ ( 𝑘 = 𝑥 → ( ℎ ‘ suc 𝑘 ) = ( ℎ ‘ suc 𝑥 ) )
80 77 79 breq12d ⊢ ( 𝑘 = 𝑥 → ( ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ↔ ( ℎ ‘ 𝑥 ) 𝑅 ( ℎ ‘ suc 𝑥 ) ) )
81 80 rspccv ⊢ ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) → ( 𝑥 ∈ ω → ( ℎ ‘ 𝑥 ) 𝑅 ( ℎ ‘ suc 𝑥 ) ) )
82 fvex ⊢ ( ℎ ‘ 𝑥 ) ∈ V
83 fvex ⊢ ( ℎ ‘ suc 𝑥 ) ∈ V
84 82 83 breldm ⊢ ( ( ℎ ‘ 𝑥 ) 𝑅 ( ℎ ‘ suc 𝑥 ) → ( ℎ ‘ 𝑥 ) ∈ dom 𝑅 )
85 81 84 syl6 ⊢ ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) → ( 𝑥 ∈ ω → ( ℎ ‘ 𝑥 ) ∈ dom 𝑅 ) )
86 85 imp ⊢ ( ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ∧ 𝑥 ∈ ω ) → ( ℎ ‘ 𝑥 ) ∈ dom 𝑅 )
87 86 adantll ⊢ ( ( ( dom 𝑅 = 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) ∧ 𝑥 ∈ ω ) → ( ℎ ‘ 𝑥 ) ∈ dom 𝑅 )
88 eleq2 ⊢ ( dom 𝑅 = 𝐴 → ( ( ℎ ‘ 𝑥 ) ∈ dom 𝑅 ↔ ( ℎ ‘ 𝑥 ) ∈ 𝐴 ) )
89 88 ad2antrr ⊢ ( ( ( dom 𝑅 = 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) ∧ 𝑥 ∈ ω ) → ( ( ℎ ‘ 𝑥 ) ∈ dom 𝑅 ↔ ( ℎ ‘ 𝑥 ) ∈ 𝐴 ) )
90 87 89 mpbid ⊢ ( ( ( dom 𝑅 = 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) ∧ 𝑥 ∈ ω ) → ( ℎ ‘ 𝑥 ) ∈ 𝐴 )
91 90 3 fmptd ⊢ ( ( dom 𝑅 = 𝐴 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) → 𝐺 : ω ⟶ 𝐴 )
92 91 ex ⊢ ( dom 𝑅 = 𝐴 → ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) → 𝐺 : ω ⟶ 𝐴 ) )
93 19 92 syl ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) → 𝐺 : ω ⟶ 𝐴 ) )
94 93 impcom ⊢ ( ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → 𝐺 : ω ⟶ 𝐴 )
95 fveq2 ⊢ ( 𝑥 = 𝑘 → ( ℎ ‘ 𝑥 ) = ( ℎ ‘ 𝑘 ) )
96 fvex ⊢ ( ℎ ‘ 𝑘 ) ∈ V
97 95 3 96 fvmpt ⊢ ( 𝑘 ∈ ω → ( 𝐺 ‘ 𝑘 ) = ( ℎ ‘ 𝑘 ) )
98 peano2 ⊢ ( 𝑘 ∈ ω → suc 𝑘 ∈ ω )
99 fvex ⊢ ( ℎ ‘ suc 𝑘 ) ∈ V
100 fveq2 ⊢ ( 𝑥 = suc 𝑘 → ( ℎ ‘ 𝑥 ) = ( ℎ ‘ suc 𝑘 ) )
101 100 3 fvmptg ⊢ ( ( suc 𝑘 ∈ ω ∧ ( ℎ ‘ suc 𝑘 ) ∈ V ) → ( 𝐺 ‘ suc 𝑘 ) = ( ℎ ‘ suc 𝑘 ) )
102 98 99 101 sylancl ⊢ ( 𝑘 ∈ ω → ( 𝐺 ‘ suc 𝑘 ) = ( ℎ ‘ suc 𝑘 ) )
103 97 102 breq12d ⊢ ( 𝑘 ∈ ω → ( ( 𝐺 ‘ 𝑘 ) 𝑅 ( 𝐺 ‘ suc 𝑘 ) ↔ ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ) )
104 fvex ⊢ ( 𝐺 ‘ 𝑘 ) ∈ V
105 fvex ⊢ ( 𝐺 ‘ suc 𝑘 ) ∈ V
106 eleq1 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑘 ) → ( 𝑥 ∈ 𝐴 ↔ ( 𝐺 ‘ 𝑘 ) ∈ 𝐴 ) )
107 fveq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑘 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
108 107 eleq2d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑘 ) → ( 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
109 106 108 anbi12d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑘 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝐺 ‘ 𝑘 ) ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) )
110 eleq1 ⊢ ( 𝑦 = ( 𝐺 ‘ suc 𝑘 ) → ( 𝑦 ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
111 110 anbi2d ⊢ ( 𝑦 = ( 𝐺 ‘ suc 𝑘 ) → ( ( ( 𝐺 ‘ 𝑘 ) ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( ( 𝐺 ‘ 𝑘 ) ∈ 𝐴 ∧ ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) )
112 104 105 109 111 2 brab ⊢ ( ( 𝐺 ‘ 𝑘 ) 𝑅 ( 𝐺 ‘ suc 𝑘 ) ↔ ( ( 𝐺 ‘ 𝑘 ) ∈ 𝐴 ∧ ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
113 112 simprbi ⊢ ( ( 𝐺 ‘ 𝑘 ) 𝑅 ( 𝐺 ‘ suc 𝑘 ) → ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
114 103 113 biimtrrdi ⊢ ( 𝑘 ∈ ω → ( ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) → ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
115 114 ralimia ⊢ ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) → ∀ 𝑘 ∈ ω ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
116 115 adantr ⊢ ( ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∀ 𝑘 ∈ ω ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
117 fvrn0 ⊢ ( ℎ ‘ 𝑥 ) ∈ ( ran ℎ ∪ { ∅ } )
118 117 rgenw ⊢ ∀ 𝑥 ∈ ω ( ℎ ‘ 𝑥 ) ∈ ( ran ℎ ∪ { ∅ } )
119 eqid ⊢ ( 𝑥 ∈ ω ↦ ( ℎ ‘ 𝑥 ) ) = ( 𝑥 ∈ ω ↦ ( ℎ ‘ 𝑥 ) )
120 119 fmpt ⊢ ( ∀ 𝑥 ∈ ω ( ℎ ‘ 𝑥 ) ∈ ( ran ℎ ∪ { ∅ } ) ↔ ( 𝑥 ∈ ω ↦ ( ℎ ‘ 𝑥 ) ) : ω ⟶ ( ran ℎ ∪ { ∅ } ) )
121 118 120 mpbi ⊢ ( 𝑥 ∈ ω ↦ ( ℎ ‘ 𝑥 ) ) : ω ⟶ ( ran ℎ ∪ { ∅ } )
122 dcomex ⊢ ω ∈ V
123 vex ⊢ ℎ ∈ V
124 123 rnex ⊢ ran ℎ ∈ V
125 124 49 unex ⊢ ( ran ℎ ∪ { ∅ } ) ∈ V
126 fex2 ⊢ ( ( ( 𝑥 ∈ ω ↦ ( ℎ ‘ 𝑥 ) ) : ω ⟶ ( ran ℎ ∪ { ∅ } ) ∧ ω ∈ V ∧ ( ran ℎ ∪ { ∅ } ) ∈ V ) → ( 𝑥 ∈ ω ↦ ( ℎ ‘ 𝑥 ) ) ∈ V )
127 121 122 125 126 mp3an ⊢ ( 𝑥 ∈ ω ↦ ( ℎ ‘ 𝑥 ) ) ∈ V
128 3 127 eqeltri ⊢ 𝐺 ∈ V
129 feq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 : ω ⟶ 𝐴 ↔ 𝐺 : ω ⟶ 𝐴 ) )
130 fveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ suc 𝑘 ) = ( 𝐺 ‘ suc 𝑘 ) )
131 fveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
132 131 fveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
133 130 132 eleq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ↔ ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
134 133 ralbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ ω ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
135 129 134 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) ↔ ( 𝐺 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) ) )
136 128 135 spcev ⊢ ( ( 𝐺 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝐺 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )
137 94 116 136 syl2anc ⊢ ( ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )
138 137 ex ⊢ ( ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) → ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) )
139 138 exlimiv ⊢ ( ∃ ℎ ∀ 𝑘 ∈ ω ( ℎ ‘ 𝑘 ) 𝑅 ( ℎ ‘ suc 𝑘 ) → ( 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) )
140 75 76 139 sylc ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )