Metamath Proof Explorer

Theorem axdc3lem2

Description: Lemma for axdc3 . We have constructed a "candidate set" S , which consists of all finite sequences s that satisfy our property of interest, namely s ( x + 1 ) e. F ( s ( x ) ) on its domain, but with the added constraint that s ( 0 ) = C . These sets are possible "initial segments" of theinfinite sequence satisfying these constraints, but we can leverage the standard ax-dc (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely ( hn ) : m --> A (for some integer m ). We let our "choice" function select a sequence whose domain is one more than the last one, and agrees with the previous one on its domain. Thus, the application of vanilla ax-dc yields a sequence of sequences whose domains increase without bound, and whose union is a function which has all the properties we want. In this lemma, we show that given the sequence h , we can construct the sequence g that we are after. (Contributed by Mario Carneiro, 30-Jan-2013)

Ref Expression
Hypotheses axdc3lem2.1 ⊢ 𝐴 ∈ V
axdc3lem2.2 ⊢ 𝑆 = { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
axdc3lem2.3 ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } )
Assertion axdc3lem2 ( ∃ ℎ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc3lem2.1 ⊢ 𝐴 ∈ V
2 axdc3lem2.2 ⊢ 𝑆 = { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
3 axdc3lem2.3 ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } )
4 id ⊢ ( 𝑚 = ∅ → 𝑚 = ∅ )
5 fveq2 ⊢ ( 𝑚 = ∅ → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ ∅ ) )
6 5 dmeqd ⊢ ( 𝑚 = ∅ → dom ( ℎ ‘ 𝑚 ) = dom ( ℎ ‘ ∅ ) )
7 4 6 eleq12d ⊢ ( 𝑚 = ∅ → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ↔ ∅ ∈ dom ( ℎ ‘ ∅ ) ) )
8 eleq2 ⊢ ( 𝑚 = ∅ → ( 𝑗 ∈ 𝑚 ↔ 𝑗 ∈ ∅ ) )
9 5 sseq2d ⊢ ( 𝑚 = ∅ → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) )
10 8 9 imbi12d ⊢ ( 𝑚 = ∅ → ( ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ↔ ( 𝑗 ∈ ∅ → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) ) )
11 7 10 anbi12d ⊢ ( 𝑚 = ∅ → ( ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ∧ ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) ↔ ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ ( 𝑗 ∈ ∅ → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) ) ) )
12 id ⊢ ( 𝑚 = 𝑖 → 𝑚 = 𝑖 )
13 fveq2 ⊢ ( 𝑚 = 𝑖 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ 𝑖 ) )
14 13 dmeqd ⊢ ( 𝑚 = 𝑖 → dom ( ℎ ‘ 𝑚 ) = dom ( ℎ ‘ 𝑖 ) )
15 12 14 eleq12d ⊢ ( 𝑚 = 𝑖 → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ↔ 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ) )
16 elequ2 ⊢ ( 𝑚 = 𝑖 → ( 𝑗 ∈ 𝑚 ↔ 𝑗 ∈ 𝑖 ) )
17 13 sseq2d ⊢ ( 𝑚 = 𝑖 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) )
18 16 17 imbi12d ⊢ ( 𝑚 = 𝑖 → ( ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ↔ ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) )
19 15 18 anbi12d ⊢ ( 𝑚 = 𝑖 → ( ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ∧ ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) ↔ ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) ) )
20 id ⊢ ( 𝑚 = suc 𝑖 → 𝑚 = suc 𝑖 )
21 fveq2 ⊢ ( 𝑚 = suc 𝑖 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ suc 𝑖 ) )
22 21 dmeqd ⊢ ( 𝑚 = suc 𝑖 → dom ( ℎ ‘ 𝑚 ) = dom ( ℎ ‘ suc 𝑖 ) )
23 20 22 eleq12d ⊢ ( 𝑚 = suc 𝑖 → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ↔ suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ) )
24 eleq2 ⊢ ( 𝑚 = suc 𝑖 → ( 𝑗 ∈ 𝑚 ↔ 𝑗 ∈ suc 𝑖 ) )
25 21 sseq2d ⊢ ( 𝑚 = suc 𝑖 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) )
26 24 25 imbi12d ⊢ ( 𝑚 = suc 𝑖 → ( ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ↔ ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) )
27 23 26 anbi12d ⊢ ( 𝑚 = suc 𝑖 → ( ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ∧ ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) ↔ ( suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ∧ ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) )
28 peano1 ⊢ ∅ ∈ ω
29 ffvelcdm ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∅ ∈ ω ) → ( ℎ ‘ ∅ ) ∈ 𝑆 )
30 28 29 mpan2 ⊢ ( ℎ : ω ⟶ 𝑆 → ( ℎ ‘ ∅ ) ∈ 𝑆 )
31 fdm ⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → dom 𝑠 = suc 𝑛 )
32 nnord ⊢ ( 𝑛 ∈ ω → Ord 𝑛 )
33 0elsuc ⊢ ( Ord 𝑛 → ∅ ∈ suc 𝑛 )
34 32 33 syl ⊢ ( 𝑛 ∈ ω → ∅ ∈ suc 𝑛 )
35 peano2 ⊢ ( 𝑛 ∈ ω → suc 𝑛 ∈ ω )
36 eleq2 ⊢ ( dom 𝑠 = suc 𝑛 → ( ∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛 ) )
37 eleq1 ⊢ ( dom 𝑠 = suc 𝑛 → ( dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω ) )
38 36 37 anbi12d ⊢ ( dom 𝑠 = suc 𝑛 → ( ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ↔ ( ∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω ) ) )
39 38 biimprcd ⊢ ( ( ∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω ) → ( dom 𝑠 = suc 𝑛 → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ) )
40 34 35 39 syl2anc ⊢ ( 𝑛 ∈ ω → ( dom 𝑠 = suc 𝑛 → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ) )
41 31 40 syl5com ⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → ( 𝑛 ∈ ω → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ) )
42 41 3ad2ant1 ⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑛 ∈ ω → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ) )
43 42 impcom ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) )
44 43 rexlimiva ⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) )
45 44 ss2abi ⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) }
46 2 45 eqsstri ⊢ 𝑆 ⊆ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) }
47 46 sseli ⊢ ( ( ℎ ‘ ∅ ) ∈ 𝑆 → ( ℎ ‘ ∅ ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } )
48 fvex ⊢ ( ℎ ‘ ∅ ) ∈ V
49 dmeq ⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → dom 𝑠 = dom ( ℎ ‘ ∅ ) )
50 49 eleq2d ⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → ( ∅ ∈ dom 𝑠 ↔ ∅ ∈ dom ( ℎ ‘ ∅ ) ) )
51 49 eleq1d ⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → ( dom 𝑠 ∈ ω ↔ dom ( ℎ ‘ ∅ ) ∈ ω ) )
52 50 51 anbi12d ⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → ( ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ↔ ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ dom ( ℎ ‘ ∅ ) ∈ ω ) ) )
53 48 52 elab ⊢ ( ( ℎ ‘ ∅ ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ↔ ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ dom ( ℎ ‘ ∅ ) ∈ ω ) )
54 47 53 sylib ⊢ ( ( ℎ ‘ ∅ ) ∈ 𝑆 → ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ dom ( ℎ ‘ ∅ ) ∈ ω ) )
55 54 simpld ⊢ ( ( ℎ ‘ ∅ ) ∈ 𝑆 → ∅ ∈ dom ( ℎ ‘ ∅ ) )
56 30 55 syl ⊢ ( ℎ : ω ⟶ 𝑆 → ∅ ∈ dom ( ℎ ‘ ∅ ) )
57 noel ⊢ ¬ 𝑗 ∈ ∅
58 57 pm2.21i ⊢ ( 𝑗 ∈ ∅ → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) )
59 56 58 jctir ⊢ ( ℎ : ω ⟶ 𝑆 → ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ ( 𝑗 ∈ ∅ → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) ) )
60 59 adantr ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ ( 𝑗 ∈ ∅ → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) ) )
61 ffvelcdm ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑖 ∈ ω ) → ( ℎ ‘ 𝑖 ) ∈ 𝑆 )
62 61 ancoms ⊢ ( ( 𝑖 ∈ ω ∧ ℎ : ω ⟶ 𝑆 ) → ( ℎ ‘ 𝑖 ) ∈ 𝑆 )
63 62 adantrr ⊢ ( ( 𝑖 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ℎ ‘ 𝑖 ) ∈ 𝑆 )
64 suceq ⊢ ( 𝑘 = 𝑖 → suc 𝑘 = suc 𝑖 )
65 64 fveq2d ⊢ ( 𝑘 = 𝑖 → ( ℎ ‘ suc 𝑘 ) = ( ℎ ‘ suc 𝑖 ) )
66 2fveq3 ⊢ ( 𝑘 = 𝑖 → ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) = ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) )
67 65 66 eleq12d ⊢ ( 𝑘 = 𝑖 → ( ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ↔ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) )
68 67 rspcva ⊢ ( ( 𝑖 ∈ ω ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) )
69 68 adantrl ⊢ ( ( 𝑖 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) )
70 46 sseli ⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( ℎ ‘ 𝑖 ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } )
71 fvex ⊢ ( ℎ ‘ 𝑖 ) ∈ V
72 dmeq ⊢ ( 𝑠 = ( ℎ ‘ 𝑖 ) → dom 𝑠 = dom ( ℎ ‘ 𝑖 ) )
73 72 eleq2d ⊢ ( 𝑠 = ( ℎ ‘ 𝑖 ) → ( ∅ ∈ dom 𝑠 ↔ ∅ ∈ dom ( ℎ ‘ 𝑖 ) ) )
74 72 eleq1d ⊢ ( 𝑠 = ( ℎ ‘ 𝑖 ) → ( dom 𝑠 ∈ ω ↔ dom ( ℎ ‘ 𝑖 ) ∈ ω ) )
75 73 74 anbi12d ⊢ ( 𝑠 = ( ℎ ‘ 𝑖 ) → ( ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ↔ ( ∅ ∈ dom ( ℎ ‘ 𝑖 ) ∧ dom ( ℎ ‘ 𝑖 ) ∈ ω ) ) )
76 71 75 elab ⊢ ( ( ℎ ‘ 𝑖 ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ↔ ( ∅ ∈ dom ( ℎ ‘ 𝑖 ) ∧ dom ( ℎ ‘ 𝑖 ) ∈ ω ) )
77 70 76 sylib ⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( ∅ ∈ dom ( ℎ ‘ 𝑖 ) ∧ dom ( ℎ ‘ 𝑖 ) ∈ ω ) )
78 77 simprd ⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → dom ( ℎ ‘ 𝑖 ) ∈ ω )
79 nnord ⊢ ( dom ( ℎ ‘ 𝑖 ) ∈ ω → Ord dom ( ℎ ‘ 𝑖 ) )
80 ordsucelsuc ⊢ ( Ord dom ( ℎ ‘ 𝑖 ) → ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ↔ suc 𝑖 ∈ suc dom ( ℎ ‘ 𝑖 ) ) )
81 78 79 80 3syl ⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ↔ suc 𝑖 ∈ suc dom ( ℎ ‘ 𝑖 ) ) )
82 81 adantr ⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ↔ suc 𝑖 ∈ suc dom ( ℎ ‘ 𝑖 ) ) )
83 dmeq ⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → dom 𝑥 = dom ( ℎ ‘ 𝑖 ) )
84 suceq ⊢ ( dom 𝑥 = dom ( ℎ ‘ 𝑖 ) → suc dom 𝑥 = suc dom ( ℎ ‘ 𝑖 ) )
85 83 84 syl ⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → suc dom 𝑥 = suc dom ( ℎ ‘ 𝑖 ) )
86 85 eqeq2d ⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → ( dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ) )
87 83 reseq2d ⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → ( 𝑦 ↾ dom 𝑥 ) = ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) )
88 id ⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → 𝑥 = ( ℎ ‘ 𝑖 ) )
89 87 88 eqeq12d ⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → ( ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ↔ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) )
90 86 89 anbi12d ⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → ( ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ↔ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) )
91 90 rabbidv ⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } = { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) } )
92 1 2 axdc3lem ⊢ 𝑆 ∈ V
93 92 rabex ⊢ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) } ∈ V
94 91 3 93 fvmpt ⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) = { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) } )
95 94 eleq2d ⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ↔ ( ℎ ‘ suc 𝑖 ) ∈ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) } ) )
96 dmeq ⊢ ( 𝑦 = ( ℎ ‘ suc 𝑖 ) → dom 𝑦 = dom ( ℎ ‘ suc 𝑖 ) )
97 96 eqeq1d ⊢ ( 𝑦 = ( ℎ ‘ suc 𝑖 ) → ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ↔ dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ) )
98 reseq1 ⊢ ( 𝑦 = ( ℎ ‘ suc 𝑖 ) → ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) )
99 98 eqeq1d ⊢ ( 𝑦 = ( ℎ ‘ suc 𝑖 ) → ( ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ↔ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) )
100 97 99 anbi12d ⊢ ( 𝑦 = ( ℎ ‘ suc 𝑖 ) → ( ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ↔ ( dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ∧ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) )
101 100 elrab ⊢ ( ( ℎ ‘ suc 𝑖 ) ∈ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) } ↔ ( ( ℎ ‘ suc 𝑖 ) ∈ 𝑆 ∧ ( dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ∧ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) )
102 95 101 bitrdi ⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ↔ ( ( ℎ ‘ suc 𝑖 ) ∈ 𝑆 ∧ ( dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ∧ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) ) )
103 102 simplbda ⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ∧ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) )
104 103 simpld ⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) )
105 104 eleq2d ⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ↔ suc 𝑖 ∈ suc dom ( ℎ ‘ 𝑖 ) ) )
106 82 105 bitr4d ⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ↔ suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ) )
107 106 biimpd ⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) → suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ) )
108 103 simprd ⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) )
109 resss ⊢ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) ⊆ ( ℎ ‘ suc 𝑖 )
110 sseq1 ⊢ ( ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) → ( ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) ⊆ ( ℎ ‘ suc 𝑖 ) ↔ ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) )
111 109 110 mpbii ⊢ ( ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) → ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) )
112 elsuci ⊢ ( 𝑗 ∈ suc 𝑖 → ( 𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖 ) )
113 pm2.27 ⊢ ( 𝑗 ∈ 𝑖 → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) )
114 sstr2 ⊢ ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) )
115 113 114 syl6 ⊢ ( 𝑗 ∈ 𝑖 → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) )
116 fveq2 ⊢ ( 𝑗 = 𝑖 → ( ℎ ‘ 𝑗 ) = ( ℎ ‘ 𝑖 ) )
117 116 sseq1d ⊢ ( 𝑗 = 𝑖 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ↔ ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) )
118 117 biimprd ⊢ ( 𝑗 = 𝑖 → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) )
119 118 a1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) )
120 115 119 jaoi ⊢ ( ( 𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖 ) → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) )
121 112 120 syl ⊢ ( 𝑗 ∈ suc 𝑖 → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) )
122 121 com13 ⊢ ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) )
123 108 111 122 3syl ⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) )
124 107 123 anim12d ⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) → ( suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ∧ ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) )
125 63 69 124 syl2anc ⊢ ( ( 𝑖 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) → ( suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ∧ ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) )
126 125 ex ⊢ ( 𝑖 ∈ ω → ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) → ( suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ∧ ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) ) )
127 11 19 27 60 126 finds2 ⊢ ( 𝑚 ∈ ω → ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ∧ ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) ) )
128 127 imp ⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ∧ ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) )
129 128 simprd ⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) )
130 129 expcom ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ ω → ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) )
131 130 ralrimdv ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ ω → ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) )
132 131 ralrimiv ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) )
133 frn ⊢ ( ℎ : ω ⟶ 𝑆 → ran ℎ ⊆ 𝑆 )
134 ffun ⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → Fun 𝑠 )
135 134 3ad2ant1 ⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → Fun 𝑠 )
136 135 rexlimivw ⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → Fun 𝑠 )
137 136 ss2abi ⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ { 𝑠 ∣ Fun 𝑠 }
138 2 137 eqsstri ⊢ 𝑆 ⊆ { 𝑠 ∣ Fun 𝑠 }
139 133 138 sstrdi ⊢ ( ℎ : ω ⟶ 𝑆 → ran ℎ ⊆ { 𝑠 ∣ Fun 𝑠 } )
140 139 sseld ⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑢 ∈ ran ℎ → 𝑢 ∈ { 𝑠 ∣ Fun 𝑠 } ) )
141 vex ⊢ 𝑢 ∈ V
142 funeq ⊢ ( 𝑠 = 𝑢 → ( Fun 𝑠 ↔ Fun 𝑢 ) )
143 141 142 elab ⊢ ( 𝑢 ∈ { 𝑠 ∣ Fun 𝑠 } ↔ Fun 𝑢 )
144 140 143 imbitrdi ⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑢 ∈ ran ℎ → Fun 𝑢 ) )
145 144 adantr ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ( 𝑢 ∈ ran ℎ → Fun 𝑢 ) )
146 ffn ⊢ ( ℎ : ω ⟶ 𝑆 → ℎ Fn ω )
147 fvelrnb ⊢ ( ℎ Fn ω → ( 𝑣 ∈ ran ℎ ↔ ∃ 𝑏 ∈ ω ( ℎ ‘ 𝑏 ) = 𝑣 ) )
148 fvelrnb ⊢ ( ℎ Fn ω → ( 𝑢 ∈ ran ℎ ↔ ∃ 𝑎 ∈ ω ( ℎ ‘ 𝑎 ) = 𝑢 ) )
149 nnord ⊢ ( 𝑎 ∈ ω → Ord 𝑎 )
150 nnord ⊢ ( 𝑏 ∈ ω → Ord 𝑏 )
151 149 150 anim12i ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( Ord 𝑎 ∧ Ord 𝑏 ) )
152 ordtri3or ⊢ ( ( Ord 𝑎 ∧ Ord 𝑏 ) → ( 𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎 ) )
153 fveq2 ⊢ ( 𝑚 = 𝑏 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ 𝑏 ) )
154 153 sseq2d ⊢ ( 𝑚 = 𝑏 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑏 ) ) )
155 154 raleqbi1dv ⊢ ( 𝑚 = 𝑏 → ( ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ∀ 𝑗 ∈ 𝑏 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑏 ) ) )
156 155 rspcv ⊢ ( 𝑏 ∈ ω → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ∀ 𝑗 ∈ 𝑏 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑏 ) ) )
157 fveq2 ⊢ ( 𝑗 = 𝑎 → ( ℎ ‘ 𝑗 ) = ( ℎ ‘ 𝑎 ) )
158 157 sseq1d ⊢ ( 𝑗 = 𝑎 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑏 ) ↔ ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ) )
159 158 rspccv ⊢ ( ∀ 𝑗 ∈ 𝑏 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑏 ) → ( 𝑎 ∈ 𝑏 → ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ) )
160 156 159 syl6 ⊢ ( 𝑏 ∈ ω → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑎 ∈ 𝑏 → ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ) ) )
161 160 adantl ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑎 ∈ 𝑏 → ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ) ) )
162 161 3imp ⊢ ( ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ∧ 𝑎 ∈ 𝑏 ) → ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) )
163 162 orcd ⊢ ( ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ∧ 𝑎 ∈ 𝑏 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) )
164 163 3exp ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑎 ∈ 𝑏 → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) )
165 164 com3r ⊢ ( 𝑎 ∈ 𝑏 → ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) )
166 fveq2 ⊢ ( 𝑎 = 𝑏 → ( ℎ ‘ 𝑎 ) = ( ℎ ‘ 𝑏 ) )
167 eqimss ⊢ ( ( ℎ ‘ 𝑎 ) = ( ℎ ‘ 𝑏 ) → ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) )
168 167 orcd ⊢ ( ( ℎ ‘ 𝑎 ) = ( ℎ ‘ 𝑏 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) )
169 166 168 syl ⊢ ( 𝑎 = 𝑏 → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) )
170 169 2a1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) )
171 fveq2 ⊢ ( 𝑚 = 𝑎 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ 𝑎 ) )
172 171 sseq2d ⊢ ( 𝑚 = 𝑎 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑎 ) ) )
173 172 raleqbi1dv ⊢ ( 𝑚 = 𝑎 → ( ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ∀ 𝑗 ∈ 𝑎 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑎 ) ) )
174 173 rspcv ⊢ ( 𝑎 ∈ ω → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ∀ 𝑗 ∈ 𝑎 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑎 ) ) )
175 fveq2 ⊢ ( 𝑗 = 𝑏 → ( ℎ ‘ 𝑗 ) = ( ℎ ‘ 𝑏 ) )
176 175 sseq1d ⊢ ( 𝑗 = 𝑏 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑎 ) ↔ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) )
177 176 rspccv ⊢ ( ∀ 𝑗 ∈ 𝑎 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑎 ) → ( 𝑏 ∈ 𝑎 → ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) )
178 174 177 syl6 ⊢ ( 𝑎 ∈ ω → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑏 ∈ 𝑎 → ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) )
179 178 adantr ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑏 ∈ 𝑎 → ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) )
180 179 3imp ⊢ ( ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ∧ 𝑏 ∈ 𝑎 ) → ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) )
181 180 olcd ⊢ ( ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ∧ 𝑏 ∈ 𝑎 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) )
182 181 3exp ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑏 ∈ 𝑎 → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) )
183 182 com3r ⊢ ( 𝑏 ∈ 𝑎 → ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) )
184 165 170 183 3jaoi ⊢ ( ( 𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎 ) → ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) )
185 152 184 syl ⊢ ( ( Ord 𝑎 ∧ Ord 𝑏 ) → ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) )
186 151 185 mpcom ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) )
187 sseq12 ⊢ ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ↔ 𝑢 ⊆ 𝑣 ) )
188 sseq12 ⊢ ( ( ( ℎ ‘ 𝑏 ) = 𝑣 ∧ ( ℎ ‘ 𝑎 ) = 𝑢 ) → ( ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ↔ 𝑣 ⊆ 𝑢 ) )
189 188 ancoms ⊢ ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ↔ 𝑣 ⊆ 𝑢 ) )
190 187 189 orbi12d ⊢ ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ↔ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
191 190 biimpcd ⊢ ( ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) → ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
192 186 191 syl6 ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) )
193 192 com23 ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) )
194 193 exp4b ⊢ ( 𝑎 ∈ ω → ( 𝑏 ∈ ω → ( ( ℎ ‘ 𝑎 ) = 𝑢 → ( ( ℎ ‘ 𝑏 ) = 𝑣 → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) ) )
195 194 com23 ⊢ ( 𝑎 ∈ ω → ( ( ℎ ‘ 𝑎 ) = 𝑢 → ( 𝑏 ∈ ω → ( ( ℎ ‘ 𝑏 ) = 𝑣 → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) ) )
196 195 rexlimiv ⊢ ( ∃ 𝑎 ∈ ω ( ℎ ‘ 𝑎 ) = 𝑢 → ( 𝑏 ∈ ω → ( ( ℎ ‘ 𝑏 ) = 𝑣 → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) )
197 196 rexlimdv ⊢ ( ∃ 𝑎 ∈ ω ( ℎ ‘ 𝑎 ) = 𝑢 → ( ∃ 𝑏 ∈ ω ( ℎ ‘ 𝑏 ) = 𝑣 → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) )
198 148 197 biimtrdi ⊢ ( ℎ Fn ω → ( 𝑢 ∈ ran ℎ → ( ∃ 𝑏 ∈ ω ( ℎ ‘ 𝑏 ) = 𝑣 → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) )
199 198 com23 ⊢ ( ℎ Fn ω → ( ∃ 𝑏 ∈ ω ( ℎ ‘ 𝑏 ) = 𝑣 → ( 𝑢 ∈ ran ℎ → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) )
200 147 199 sylbid ⊢ ( ℎ Fn ω → ( 𝑣 ∈ ran ℎ → ( 𝑢 ∈ ran ℎ → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) )
201 200 com24 ⊢ ( ℎ Fn ω → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ∈ ran ℎ → ( 𝑣 ∈ ran ℎ → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) )
202 201 imp ⊢ ( ( ℎ Fn ω ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ( 𝑢 ∈ ran ℎ → ( 𝑣 ∈ ran ℎ → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) )
203 202 ralrimdv ⊢ ( ( ℎ Fn ω ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ( 𝑢 ∈ ran ℎ → ∀ 𝑣 ∈ ran ℎ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
204 146 203 sylan ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ( 𝑢 ∈ ran ℎ → ∀ 𝑣 ∈ ran ℎ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
205 145 204 jcad ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ( 𝑢 ∈ ran ℎ → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ ran ℎ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) )
206 205 ralrimiv ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ∀ 𝑢 ∈ ran ℎ ( Fun 𝑢 ∧ ∀ 𝑣 ∈ ran ℎ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) )
207 fununi ⊢ ( ∀ 𝑢 ∈ ran ℎ ( Fun 𝑢 ∧ ∀ 𝑣 ∈ ran ℎ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) → Fun ∪ ran ℎ )
208 206 207 syl ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → Fun ∪ ran ℎ )
209 132 208 syldan ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → Fun ∪ ran ℎ )
210 vex ⊢ 𝑚 ∈ V
211 210 eldm2 ⊢ ( 𝑚 ∈ dom ∪ ran ℎ ↔ ∃ 𝑢 ⟨ 𝑚 , 𝑢 ⟩ ∈ ∪ ran ℎ )
212 eluni2 ⊢ ( ⟨ 𝑚 , 𝑢 ⟩ ∈ ∪ ran ℎ ↔ ∃ 𝑣 ∈ ran ℎ ⟨ 𝑚 , 𝑢 ⟩ ∈ 𝑣 )
213 210 141 opeldm ⊢ ( ⟨ 𝑚 , 𝑢 ⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣 )
214 213 a1i ⊢ ( ℎ : ω ⟶ 𝑆 → ( ⟨ 𝑚 , 𝑢 ⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣 ) )
215 133 46 sstrdi ⊢ ( ℎ : ω ⟶ 𝑆 → ran ℎ ⊆ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } )
216 ssel ⊢ ( ran ℎ ⊆ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } → ( 𝑣 ∈ ran ℎ → 𝑣 ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ) )
217 vex ⊢ 𝑣 ∈ V
218 dmeq ⊢ ( 𝑠 = 𝑣 → dom 𝑠 = dom 𝑣 )
219 218 eleq2d ⊢ ( 𝑠 = 𝑣 → ( ∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣 ) )
220 218 eleq1d ⊢ ( 𝑠 = 𝑣 → ( dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω ) )
221 219 220 anbi12d ⊢ ( 𝑠 = 𝑣 → ( ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ↔ ( ∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω ) ) )
222 217 221 elab ⊢ ( 𝑣 ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ↔ ( ∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω ) )
223 222 simprbi ⊢ ( 𝑣 ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } → dom 𝑣 ∈ ω )
224 216 223 syl6 ⊢ ( ran ℎ ⊆ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } → ( 𝑣 ∈ ran ℎ → dom 𝑣 ∈ ω ) )
225 215 224 syl ⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑣 ∈ ran ℎ → dom 𝑣 ∈ ω ) )
226 214 225 anim12d ⊢ ( ℎ : ω ⟶ 𝑆 → ( ( ⟨ 𝑚 , 𝑢 ⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ ) → ( 𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω ) ) )
227 elnn ⊢ ( ( 𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω ) → 𝑚 ∈ ω )
228 226 227 syl6 ⊢ ( ℎ : ω ⟶ 𝑆 → ( ( ⟨ 𝑚 , 𝑢 ⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ ) → 𝑚 ∈ ω ) )
229 228 expcomd ⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑣 ∈ ran ℎ → ( ⟨ 𝑚 , 𝑢 ⟩ ∈ 𝑣 → 𝑚 ∈ ω ) ) )
230 229 rexlimdv ⊢ ( ℎ : ω ⟶ 𝑆 → ( ∃ 𝑣 ∈ ran ℎ ⟨ 𝑚 , 𝑢 ⟩ ∈ 𝑣 → 𝑚 ∈ ω ) )
231 212 230 biimtrid ⊢ ( ℎ : ω ⟶ 𝑆 → ( ⟨ 𝑚 , 𝑢 ⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω ) )
232 231 exlimdv ⊢ ( ℎ : ω ⟶ 𝑆 → ( ∃ 𝑢 ⟨ 𝑚 , 𝑢 ⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω ) )
233 211 232 biimtrid ⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω ) )
234 233 adantr ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω ) )
235 id ⊢ ( 𝑚 ∈ ω → 𝑚 ∈ ω )
236 fnfvelrn ⊢ ( ( ℎ Fn ω ∧ 𝑚 ∈ ω ) → ( ℎ ‘ 𝑚 ) ∈ ran ℎ )
237 146 235 236 syl2anr ⊢ ( ( 𝑚 ∈ ω ∧ ℎ : ω ⟶ 𝑆 ) → ( ℎ ‘ 𝑚 ) ∈ ran ℎ )
238 237 adantrr ⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ℎ ‘ 𝑚 ) ∈ ran ℎ )
239 128 simpld ⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) )
240 dmeq ⊢ ( 𝑢 = ( ℎ ‘ 𝑚 ) → dom 𝑢 = dom ( ℎ ‘ 𝑚 ) )
241 240 eliuni ⊢ ( ( ( ℎ ‘ 𝑚 ) ∈ ran ℎ ∧ 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎ dom 𝑢 )
242 238 239 241 syl2anc ⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎ dom 𝑢 )
243 dmuni ⊢ dom ∪ ran ℎ = ∪ 𝑢 ∈ ran ℎ dom 𝑢
244 242 243 eleqtrrdi ⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → 𝑚 ∈ dom ∪ ran ℎ )
245 244 expcom ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ ω → 𝑚 ∈ dom ∪ ran ℎ ) )
246 234 245 impbid ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ dom ∪ ran ℎ ↔ 𝑚 ∈ ω ) )
247 246 eqrdv ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → dom ∪ ran ℎ = ω )
248 rnuni ⊢ ran ∪ ran ℎ = ∪ 𝑠 ∈ ran ℎ ran 𝑠
249 frn ⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → ran 𝑠 ⊆ 𝐴 )
250 249 3ad2ant1 ⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ran 𝑠 ⊆ 𝐴 )
251 250 rexlimivw ⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ran 𝑠 ⊆ 𝐴 )
252 251 ss2abi ⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 }
253 2 252 eqsstri ⊢ 𝑆 ⊆ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 }
254 133 253 sstrdi ⊢ ( ℎ : ω ⟶ 𝑆 → ran ℎ ⊆ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } )
255 ssel ⊢ ( ran ℎ ⊆ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } → ( 𝑠 ∈ ran ℎ → 𝑠 ∈ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } ) )
256 abid ⊢ ( 𝑠 ∈ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } ↔ ran 𝑠 ⊆ 𝐴 )
257 255 256 imbitrdi ⊢ ( ran ℎ ⊆ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } → ( 𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴 ) )
258 254 257 syl ⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴 ) )
259 258 ralrimiv ⊢ ( ℎ : ω ⟶ 𝑆 → ∀ 𝑠 ∈ ran ℎ ran 𝑠 ⊆ 𝐴 )
260 iunss ⊢ ( ∪ 𝑠 ∈ ran ℎ ran 𝑠 ⊆ 𝐴 ↔ ∀ 𝑠 ∈ ran ℎ ran 𝑠 ⊆ 𝐴 )
261 259 260 sylibr ⊢ ( ℎ : ω ⟶ 𝑆 → ∪ 𝑠 ∈ ran ℎ ran 𝑠 ⊆ 𝐴 )
262 248 261 eqsstrid ⊢ ( ℎ : ω ⟶ 𝑆 → ran ∪ ran ℎ ⊆ 𝐴 )
263 262 adantr ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ran ∪ ran ℎ ⊆ 𝐴 )
264 df-fn ⊢ ( ∪ ran ℎ Fn ω ↔ ( Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω ) )
265 df-f ⊢ ( ∪ ran ℎ : ω ⟶ 𝐴 ↔ ( ∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴 ) )
266 265 biimpri ⊢ ( ( ∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴 ) → ∪ ran ℎ : ω ⟶ 𝐴 )
267 264 266 sylanbr ⊢ ( ( ( Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω ) ∧ ran ∪ ran ℎ ⊆ 𝐴 ) → ∪ ran ℎ : ω ⟶ 𝐴 )
268 209 247 263 267 syl21anc ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∪ ran ℎ : ω ⟶ 𝐴 )
269 fnfvelrn ⊢ ( ( ℎ Fn ω ∧ ∅ ∈ ω ) → ( ℎ ‘ ∅ ) ∈ ran ℎ )
270 146 28 269 sylancl ⊢ ( ℎ : ω ⟶ 𝑆 → ( ℎ ‘ ∅ ) ∈ ran ℎ )
271 270 adantr ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ℎ ‘ ∅ ) ∈ ran ℎ )
272 elssuni ⊢ ( ( ℎ ‘ ∅ ) ∈ ran ℎ → ( ℎ ‘ ∅ ) ⊆ ∪ ran ℎ )
273 271 272 syl ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ℎ ‘ ∅ ) ⊆ ∪ ran ℎ )
274 56 adantr ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∅ ∈ dom ( ℎ ‘ ∅ ) )
275 funssfv ⊢ ( ( Fun ∪ ran ℎ ∧ ( ℎ ‘ ∅ ) ⊆ ∪ ran ℎ ∧ ∅ ∈ dom ( ℎ ‘ ∅ ) ) → ( ∪ ran ℎ ‘ ∅ ) = ( ( ℎ ‘ ∅ ) ‘ ∅ ) )
276 209 273 274 275 syl3anc ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ∪ ran ℎ ‘ ∅ ) = ( ( ℎ ‘ ∅ ) ‘ ∅ ) )
277 simp2 ⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑠 ‘ ∅ ) = 𝐶 )
278 277 rexlimivw ⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑠 ‘ ∅ ) = 𝐶 )
279 278 ss2abi ⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 }
280 2 279 eqsstri ⊢ 𝑆 ⊆ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 }
281 133 280 sstrdi ⊢ ( ℎ : ω ⟶ 𝑆 → ran ℎ ⊆ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } )
282 ssel ⊢ ( ran ℎ ⊆ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } → ( ( ℎ ‘ ∅ ) ∈ ran ℎ → ( ℎ ‘ ∅ ) ∈ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } ) )
283 fveq1 ⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → ( 𝑠 ‘ ∅ ) = ( ( ℎ ‘ ∅ ) ‘ ∅ ) )
284 283 eqeq1d ⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → ( ( 𝑠 ‘ ∅ ) = 𝐶 ↔ ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 ) )
285 48 284 elab ⊢ ( ( ℎ ‘ ∅ ) ∈ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } ↔ ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 )
286 282 285 imbitrdi ⊢ ( ran ℎ ⊆ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } → ( ( ℎ ‘ ∅ ) ∈ ran ℎ → ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 ) )
287 281 286 syl ⊢ ( ℎ : ω ⟶ 𝑆 → ( ( ℎ ‘ ∅ ) ∈ ran ℎ → ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 ) )
288 287 adantr ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ( ℎ ‘ ∅ ) ∈ ran ℎ → ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 ) )
289 271 288 mpd ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 )
290 276 289 eqtrd ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ∪ ran ℎ ‘ ∅ ) = 𝐶 )
291 nfv ⊢ Ⅎ 𝑘 ℎ : ω ⟶ 𝑆
292 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) )
293 291 292 nfan ⊢ Ⅎ 𝑘 ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) )
294 133 ad2antrr ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ran ℎ ⊆ 𝑆 )
295 peano2 ⊢ ( 𝑘 ∈ ω → suc 𝑘 ∈ ω )
296 fnfvelrn ⊢ ( ( ℎ Fn ω ∧ suc 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ )
297 146 295 296 syl2an ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ )
298 297 adantlr ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ )
299 239 expcom ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ ω → 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ) )
300 299 ralrimiv ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∀ 𝑚 ∈ ω 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) )
301 id ⊢ ( 𝑚 = suc 𝑘 → 𝑚 = suc 𝑘 )
302 fveq2 ⊢ ( 𝑚 = suc 𝑘 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ suc 𝑘 ) )
303 302 dmeqd ⊢ ( 𝑚 = suc 𝑘 → dom ( ℎ ‘ 𝑚 ) = dom ( ℎ ‘ suc 𝑘 ) )
304 301 303 eleq12d ⊢ ( 𝑚 = suc 𝑘 → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ↔ suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) )
305 304 rspcv ⊢ ( suc 𝑘 ∈ ω → ( ∀ 𝑚 ∈ ω 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) → suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) )
306 295 305 syl ⊢ ( 𝑘 ∈ ω → ( ∀ 𝑚 ∈ ω 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) → suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) )
307 300 306 mpan9 ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) )
308 eleq2 ⊢ ( dom 𝑠 = suc 𝑛 → ( suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛 ) )
309 308 biimpa ⊢ ( ( dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠 ) → suc 𝑘 ∈ suc 𝑛 )
310 31 309 sylan ⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ suc 𝑘 ∈ dom 𝑠 ) → suc 𝑘 ∈ suc 𝑛 )
311 ordsucelsuc ⊢ ( Ord 𝑛 → ( 𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛 ) )
312 32 311 syl ⊢ ( 𝑛 ∈ ω → ( 𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛 ) )
313 312 biimprd ⊢ ( 𝑛 ∈ ω → ( suc 𝑘 ∈ suc 𝑛 → 𝑘 ∈ 𝑛 ) )
314 rsp ⊢ ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑘 ∈ 𝑛 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
315 313 314 syl9r ⊢ ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑛 ∈ ω → ( suc 𝑘 ∈ suc 𝑛 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) )
316 315 com13 ⊢ ( suc 𝑘 ∈ suc 𝑛 → ( 𝑛 ∈ ω → ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) )
317 310 316 syl ⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ suc 𝑘 ∈ dom 𝑠 ) → ( 𝑛 ∈ ω → ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) )
318 317 ex ⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑛 ∈ ω → ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) ) )
319 318 com24 ⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑛 ∈ ω → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) ) )
320 319 imp ⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑛 ∈ ω → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) )
321 320 3adant2 ⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑛 ∈ ω → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) )
322 321 impcom ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
323 322 rexlimiva ⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) )
324 323 ss2abi ⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
325 2 324 eqsstri ⊢ 𝑆 ⊆ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
326 sstr ⊢ ( ( ran ℎ ⊆ 𝑆 ∧ 𝑆 ⊆ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ) → ran ℎ ⊆ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } )
327 325 326 mpan2 ⊢ ( ran ℎ ⊆ 𝑆 → ran ℎ ⊆ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } )
328 327 sseld ⊢ ( ran ℎ ⊆ 𝑆 → ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( ℎ ‘ suc 𝑘 ) ∈ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ) )
329 fvex ⊢ ( ℎ ‘ suc 𝑘 ) ∈ V
330 dmeq ⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → dom 𝑠 = dom ( ℎ ‘ suc 𝑘 ) )
331 330 eleq2d ⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) )
332 fveq1 ⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( 𝑠 ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) )
333 fveq1 ⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( 𝑠 ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) )
334 333 fveq2d ⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) = ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) )
335 332 334 eleq12d ⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ↔ ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) )
336 331 335 imbi12d ⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ↔ ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) ) )
337 329 336 elab ⊢ ( ( ℎ ‘ suc 𝑘 ) ∈ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ↔ ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) )
338 328 337 imbitrdi ⊢ ( ran ℎ ⊆ 𝑆 → ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) ) )
339 294 298 307 338 syl3c ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) )
340 209 adantr ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → Fun ∪ ran ℎ )
341 elssuni ⊢ ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( ℎ ‘ suc 𝑘 ) ⊆ ∪ ran ℎ )
342 297 341 syl ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ⊆ ∪ ran ℎ )
343 342 adantlr ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ⊆ ∪ ran ℎ )
344 funssfv ⊢ ( ( Fun ∪ ran ℎ ∧ ( ℎ ‘ suc 𝑘 ) ⊆ ∪ ran ℎ ∧ suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) → ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) )
345 340 343 307 344 syl3anc ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) )
346 215 sseld ⊢ ( ℎ : ω ⟶ 𝑆 → ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( ℎ ‘ suc 𝑘 ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ) )
347 330 eleq2d ⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( ∅ ∈ dom 𝑠 ↔ ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ) )
348 330 eleq1d ⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( dom 𝑠 ∈ ω ↔ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) )
349 347 348 anbi12d ⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ↔ ( ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ∧ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) ) )
350 329 349 elab ⊢ ( ( ℎ ‘ suc 𝑘 ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ↔ ( ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ∧ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) )
351 346 350 imbitrdi ⊢ ( ℎ : ω ⟶ 𝑆 → ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ∧ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) ) )
352 351 adantr ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ∧ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) ) )
353 297 352 mpd ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → ( ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ∧ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) )
354 353 simprd ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → dom ( ℎ ‘ suc 𝑘 ) ∈ ω )
355 nnord ⊢ ( dom ( ℎ ‘ suc 𝑘 ) ∈ ω → Ord dom ( ℎ ‘ suc 𝑘 ) )
356 ordtr ⊢ ( Ord dom ( ℎ ‘ suc 𝑘 ) → Tr dom ( ℎ ‘ suc 𝑘 ) )
357 trsuc ⊢ ( ( Tr dom ( ℎ ‘ suc 𝑘 ) ∧ suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) → 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) )
358 357 ex ⊢ ( Tr dom ( ℎ ‘ suc 𝑘 ) → ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) )
359 354 355 356 358 4syl ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) )
360 359 adantlr ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) )
361 307 360 mpd ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) )
362 funssfv ⊢ ( ( Fun ∪ ran ℎ ∧ ( ℎ ‘ suc 𝑘 ) ⊆ ∪ ran ℎ ∧ 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) → ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) )
363 340 343 361 362 syl3anc ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) )
364 simpl ⊢ ( ( ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∧ ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) → ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) )
365 simpr ⊢ ( ( ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∧ ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) → ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) )
366 365 fveq2d ⊢ ( ( ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∧ ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) → ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) = ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) )
367 364 366 eleq12d ⊢ ( ( ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∧ ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) → ( ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ↔ ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) )
368 345 363 367 syl2anc ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ↔ ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) )
369 339 368 mpbird ⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) )
370 369 ex ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑘 ∈ ω → ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) )
371 293 370 ralrimi ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ω ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) )
372 vex ⊢ ℎ ∈ V
373 372 rnex ⊢ ran ℎ ∈ V
374 373 uniex ⊢ ∪ ran ℎ ∈ V
375 feq1 ⊢ ( 𝑔 = ∪ ran ℎ → ( 𝑔 : ω ⟶ 𝐴 ↔ ∪ ran ℎ : ω ⟶ 𝐴 ) )
376 fveq1 ⊢ ( 𝑔 = ∪ ran ℎ → ( 𝑔 ‘ ∅ ) = ( ∪ ran ℎ ‘ ∅ ) )
377 376 eqeq1d ⊢ ( 𝑔 = ∪ ran ℎ → ( ( 𝑔 ‘ ∅ ) = 𝐶 ↔ ( ∪ ran ℎ ‘ ∅ ) = 𝐶 ) )
378 fveq1 ⊢ ( 𝑔 = ∪ ran ℎ → ( 𝑔 ‘ suc 𝑘 ) = ( ∪ ran ℎ ‘ suc 𝑘 ) )
379 fveq1 ⊢ ( 𝑔 = ∪ ran ℎ → ( 𝑔 ‘ 𝑘 ) = ( ∪ ran ℎ ‘ 𝑘 ) )
380 379 fveq2d ⊢ ( 𝑔 = ∪ ran ℎ → ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) = ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) )
381 378 380 eleq12d ⊢ ( 𝑔 = ∪ ran ℎ → ( ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ↔ ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) )
382 381 ralbidv ⊢ ( 𝑔 = ∪ ran ℎ → ( ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ ω ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) )
383 375 377 382 3anbi123d ⊢ ( 𝑔 = ∪ ran ℎ → ( ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) ↔ ( ∪ ran ℎ : ω ⟶ 𝐴 ∧ ( ∪ ran ℎ ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) ) )
384 374 383 spcev ⊢ ( ( ∪ ran ℎ : ω ⟶ 𝐴 ∧ ( ∪ ran ℎ ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )
385 268 290 371 384 syl3anc ⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )
386 385 exlimiv ⊢ ( ∃ ℎ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) )