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 ffvelrn ( ( : ω ⟶ 𝑆 ∧ ∅ ∈ ω ) → ( ‘ ∅ ) ∈ 𝑆 )
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 ffvelrn ( ( : ω ⟶ 𝑆𝑖 ∈ ω ) → ( 𝑖 ) ∈ 𝑆 )
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 syl6ib ( : ω ⟶ 𝑆 → ( 𝑢 ∈ 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 syl6bi ( 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 syl5bi ( : ω ⟶ 𝑆 → ( ⟨ 𝑚 , 𝑢 ⟩ ∈ ran 𝑚 ∈ ω ) )
232 231 exlimdv ( : ω ⟶ 𝑆 → ( ∃ 𝑢𝑚 , 𝑢 ⟩ ∈ ran 𝑚 ∈ ω ) )
233 211 232 syl5bi ( : ω ⟶ 𝑆 → ( 𝑚 ∈ 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 syl6ib ( 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 syl6ib ( 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 syl6ib ( 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 syl6ib ( : ω ⟶ 𝑆 → ( ( ‘ 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 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔𝑘 ) ) ) )