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