MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axdc3lem2 Structured version   Visualization version   GIF version

Theorem axdc3lem2 9225
Description: Lemma for axdc3 9228. We have constructed a "candidate set" 𝑆, which consists of all finite sequences 𝑠 that satisfy our property of interest, namely 𝑠(𝑥 + 1) ∈ 𝐹(𝑠(𝑥)) on its domain, but with the added constraint that 𝑠(0) = 𝐶. These sets are possible "initial segments" of the infinite sequence satisfying these constraints, but we can leverage the standard ax-dc 9220 (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely (𝑛):𝑚𝐴 (for some integer 𝑚). 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 9220 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 , we can construct the sequence 𝑔 that we are after. (Contributed by Mario Carneiro, 30-Jan-2013.)
Hypotheses
Ref Expression
axdc3lem2.1 𝐴 ∈ V
axdc3lem2.2 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
axdc3lem2.3 𝐺 = (𝑥𝑆 ↦ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
Assertion
Ref Expression
axdc3lem2 (∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Distinct variable groups:   𝐴,𝑔,   𝐴,𝑛,𝑠   𝐶,𝑔,   𝐶,𝑛,𝑠   𝑔,𝐹,   𝑛,𝐹,𝑠   𝑘,𝐺   𝑆,𝑘,𝑠   𝑥,𝑆,𝑦   𝑔,𝑘,   ,𝑠   𝑥,,𝑦   𝑘,𝑛
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑘)   𝐶(𝑥,𝑦,𝑘)   𝑆(𝑔,,𝑛)   𝐹(𝑥,𝑦,𝑘)   𝐺(𝑥,𝑦,𝑔,,𝑛,𝑠)

Proof of Theorem axdc3lem2
Dummy variables 𝑖 𝑗 𝑚 𝑢 𝑣 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . . . . . . . . . . . 13 (𝑚 = ∅ → 𝑚 = ∅)
2 fveq2 6153 . . . . . . . . . . . . . 14 (𝑚 = ∅ → (𝑚) = (‘∅))
32dmeqd 5291 . . . . . . . . . . . . 13 (𝑚 = ∅ → dom (𝑚) = dom (‘∅))
41, 3eleq12d 2692 . . . . . . . . . . . 12 (𝑚 = ∅ → (𝑚 ∈ dom (𝑚) ↔ ∅ ∈ dom (‘∅)))
5 eleq2 2687 . . . . . . . . . . . . 13 (𝑚 = ∅ → (𝑗𝑚𝑗 ∈ ∅))
62sseq2d 3617 . . . . . . . . . . . . 13 (𝑚 = ∅ → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (‘∅)))
75, 6imbi12d 334 . . . . . . . . . . . 12 (𝑚 = ∅ → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
84, 7anbi12d 746 . . . . . . . . . . 11 (𝑚 = ∅ → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅)))))
9 id 22 . . . . . . . . . . . . 13 (𝑚 = 𝑖𝑚 = 𝑖)
10 fveq2 6153 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → (𝑚) = (𝑖))
1110dmeqd 5291 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → dom (𝑚) = dom (𝑖))
129, 11eleq12d 2692 . . . . . . . . . . . 12 (𝑚 = 𝑖 → (𝑚 ∈ dom (𝑚) ↔ 𝑖 ∈ dom (𝑖)))
13 elequ2 2001 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → (𝑗𝑚𝑗𝑖))
1410sseq2d 3617 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑖)))
1513, 14imbi12d 334 . . . . . . . . . . . 12 (𝑚 = 𝑖 → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗𝑖 → (𝑗) ⊆ (𝑖))))
1612, 15anbi12d 746 . . . . . . . . . . 11 (𝑚 = 𝑖 → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖)))))
17 id 22 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖𝑚 = suc 𝑖)
18 fveq2 6153 . . . . . . . . . . . . . 14 (𝑚 = suc 𝑖 → (𝑚) = (‘suc 𝑖))
1918dmeqd 5291 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → dom (𝑚) = dom (‘suc 𝑖))
2017, 19eleq12d 2692 . . . . . . . . . . . 12 (𝑚 = suc 𝑖 → (𝑚 ∈ dom (𝑚) ↔ suc 𝑖 ∈ dom (‘suc 𝑖)))
21 eleq2 2687 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → (𝑗𝑚𝑗 ∈ suc 𝑖))
2218sseq2d 3617 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (‘suc 𝑖)))
2321, 22imbi12d 334 . . . . . . . . . . . 12 (𝑚 = suc 𝑖 → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))
2420, 23anbi12d 746 . . . . . . . . . . 11 (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
25 peano1 7039 . . . . . . . . . . . . . . 15 ∅ ∈ ω
26 ffvelrn 6318 . . . . . . . . . . . . . . 15 ((:ω⟶𝑆 ∧ ∅ ∈ ω) → (‘∅) ∈ 𝑆)
2725, 26mpan2 706 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (‘∅) ∈ 𝑆)
28 axdc3lem2.2 . . . . . . . . . . . . . . . . . 18 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
29 fdm 6013 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠:suc 𝑛𝐴 → dom 𝑠 = suc 𝑛)
30 nnord 7027 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ω → Ord 𝑛)
31 0elsuc 6989 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝑛 → ∅ ∈ suc 𝑛)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → ∅ ∈ suc 𝑛)
33 peano2 7040 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
34 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛))
35 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω))
3634, 35anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom 𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω)))
3736biimprcd 240 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
3832, 33, 37syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ω → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
3929, 38syl5com 31 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠:suc 𝑛𝐴 → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
40393ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
4140impcom 446 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
4241rexlimiva 3022 . . . . . . . . . . . . . . . . . . 19 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
4342ss2abi 3658 . . . . . . . . . . . . . . . . . 18 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
4428, 43eqsstri 3619 . . . . . . . . . . . . . . . . 17 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
4544sseli 3583 . . . . . . . . . . . . . . . 16 ((‘∅) ∈ 𝑆 → (‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
46 fvex 6163 . . . . . . . . . . . . . . . . 17 (‘∅) ∈ V
47 dmeq 5289 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (‘∅) → dom 𝑠 = dom (‘∅))
4847eleq2d 2684 . . . . . . . . . . . . . . . . . 18 (𝑠 = (‘∅) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (‘∅)))
4947eleq1d 2683 . . . . . . . . . . . . . . . . . 18 (𝑠 = (‘∅) → (dom 𝑠 ∈ ω ↔ dom (‘∅) ∈ ω))
5048, 49anbi12d 746 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘∅) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω)))
5146, 50elab 3337 . . . . . . . . . . . . . . . 16 ((‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω))
5245, 51sylib 208 . . . . . . . . . . . . . . 15 ((‘∅) ∈ 𝑆 → (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω))
5352simpld 475 . . . . . . . . . . . . . 14 ((‘∅) ∈ 𝑆 → ∅ ∈ dom (‘∅))
5427, 53syl 17 . . . . . . . . . . . . 13 (:ω⟶𝑆 → ∅ ∈ dom (‘∅))
55 noel 3900 . . . . . . . . . . . . . 14 ¬ 𝑗 ∈ ∅
5655pm2.21i 116 . . . . . . . . . . . . 13 (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))
5754, 56jctir 560 . . . . . . . . . . . 12 (:ω⟶𝑆 → (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
5857adantr 481 . . . . . . . . . . 11 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
59 ffvelrn 6318 . . . . . . . . . . . . . . 15 ((:ω⟶𝑆𝑖 ∈ ω) → (𝑖) ∈ 𝑆)
6059ancoms 469 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ :ω⟶𝑆) → (𝑖) ∈ 𝑆)
6160adantrr 752 . . . . . . . . . . . . 13 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑖) ∈ 𝑆)
62 suceq 5754 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
6362fveq2d 6157 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (‘suc 𝑘) = (‘suc 𝑖))
64 fveq2 6153 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑘) = (𝑖))
6564fveq2d 6157 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (𝐺‘(𝑘)) = (𝐺‘(𝑖)))
6663, 65eleq12d 2692 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((‘suc 𝑘) ∈ (𝐺‘(𝑘)) ↔ (‘suc 𝑖) ∈ (𝐺‘(𝑖))))
6766rspcva 3296 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘suc 𝑖) ∈ (𝐺‘(𝑖)))
6867adantrl 751 . . . . . . . . . . . . 13 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (‘suc 𝑖) ∈ (𝐺‘(𝑖)))
6944sseli 3583 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ 𝑆 → (𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
70 fvex 6163 . . . . . . . . . . . . . . . . . . . . 21 (𝑖) ∈ V
71 dmeq 5289 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑖) → dom 𝑠 = dom (𝑖))
7271eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (𝑖)))
7371eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑖) → (dom 𝑠 ∈ ω ↔ dom (𝑖) ∈ ω))
7472, 73anbi12d 746 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω)))
7570, 74elab 3337 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω))
7669, 75sylib 208 . . . . . . . . . . . . . . . . . . 19 ((𝑖) ∈ 𝑆 → (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω))
7776simprd 479 . . . . . . . . . . . . . . . . . 18 ((𝑖) ∈ 𝑆 → dom (𝑖) ∈ ω)
78 nnord 7027 . . . . . . . . . . . . . . . . . 18 (dom (𝑖) ∈ ω → Ord dom (𝑖))
79 ordsucelsuc 6976 . . . . . . . . . . . . . . . . . 18 (Ord dom (𝑖) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
8077, 78, 793syl 18 . . . . . . . . . . . . . . . . 17 ((𝑖) ∈ 𝑆 → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
8180adantr 481 . . . . . . . . . . . . . . . 16 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
82 dmeq 5289 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑖) → dom 𝑥 = dom (𝑖))
83 suceq 5754 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑥 = dom (𝑖) → suc dom 𝑥 = suc dom (𝑖))
8482, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → suc dom 𝑥 = suc dom (𝑖))
8584eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (𝑖)))
8682reseq2d 5361 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (𝑖)))
87 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → 𝑥 = (𝑖))
8886, 87eqeq12d 2636 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (𝑖)) = (𝑖)))
8985, 88anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑖) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))))
9089rabbidv 3180 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑖) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))})
91 axdc3lem2.3 . . . . . . . . . . . . . . . . . . . . . 22 𝐺 = (𝑥𝑆 ↦ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
92 axdc3lem2.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝐴 ∈ V
9392, 28axdc3lem 9224 . . . . . . . . . . . . . . . . . . . . . . 23 𝑆 ∈ V
9493rabex 4778 . . . . . . . . . . . . . . . . . . . . . 22 {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))} ∈ V
9590, 91, 94fvmpt 6244 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖) ∈ 𝑆 → (𝐺‘(𝑖)) = {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))})
9695eleq2d 2684 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ 𝑆 → ((‘suc 𝑖) ∈ (𝐺‘(𝑖)) ↔ (‘suc 𝑖) ∈ {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))}))
97 dmeq 5289 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (‘suc 𝑖) → dom 𝑦 = dom (‘suc 𝑖))
9897eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (‘suc 𝑖) → (dom 𝑦 = suc dom (𝑖) ↔ dom (‘suc 𝑖) = suc dom (𝑖)))
99 reseq1 5355 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (‘suc 𝑖) → (𝑦 ↾ dom (𝑖)) = ((‘suc 𝑖) ↾ dom (𝑖)))
10099eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (‘suc 𝑖) → ((𝑦 ↾ dom (𝑖)) = (𝑖) ↔ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))
10198, 100anbi12d 746 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (‘suc 𝑖) → ((dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖)) ↔ (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖))))
102101elrab 3350 . . . . . . . . . . . . . . . . . . . 20 ((‘suc 𝑖) ∈ {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))} ↔ ((‘suc 𝑖) ∈ 𝑆 ∧ (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖))))
10396, 102syl6bb 276 . . . . . . . . . . . . . . . . . . 19 ((𝑖) ∈ 𝑆 → ((‘suc 𝑖) ∈ (𝐺‘(𝑖)) ↔ ((‘suc 𝑖) ∈ 𝑆 ∧ (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))))
104103simplbda 653 . . . . . . . . . . . . . . . . . 18 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))
105104simpld 475 . . . . . . . . . . . . . . . . 17 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → dom (‘suc 𝑖) = suc dom (𝑖))
106105eleq2d 2684 . . . . . . . . . . . . . . . 16 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
10781, 106bitr4d 271 . . . . . . . . . . . . . . 15 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ dom (‘suc 𝑖)))
108107biimpd 219 . . . . . . . . . . . . . 14 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) → suc 𝑖 ∈ dom (‘suc 𝑖)))
109104simprd 479 . . . . . . . . . . . . . . 15 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖))
110 resss 5386 . . . . . . . . . . . . . . . 16 ((‘suc 𝑖) ↾ dom (𝑖)) ⊆ (‘suc 𝑖)
111 sseq1 3610 . . . . . . . . . . . . . . . 16 (((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖) → (((‘suc 𝑖) ↾ dom (𝑖)) ⊆ (‘suc 𝑖) ↔ (𝑖) ⊆ (‘suc 𝑖)))
112110, 111mpbii 223 . . . . . . . . . . . . . . 15 (((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖) → (𝑖) ⊆ (‘suc 𝑖))
113 elsuci 5755 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ suc 𝑖 → (𝑗𝑖𝑗 = 𝑖))
114 pm2.27 42 . . . . . . . . . . . . . . . . . . 19 (𝑗𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → (𝑗) ⊆ (𝑖)))
115 sstr2 3594 . . . . . . . . . . . . . . . . . . 19 ((𝑗) ⊆ (𝑖) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖)))
116114, 115syl6 35 . . . . . . . . . . . . . . . . . 18 (𝑗𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
117 fveq2 6153 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝑗) = (𝑖))
118117sseq1d 3616 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → ((𝑗) ⊆ (‘suc 𝑖) ↔ (𝑖) ⊆ (‘suc 𝑖)))
119118biimprd 238 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖)))
120119a1d 25 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
121116, 120jaoi 394 . . . . . . . . . . . . . . . . 17 ((𝑗𝑖𝑗 = 𝑖) → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
122113, 121syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ suc 𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
123122com13 88 . . . . . . . . . . . . . . 15 ((𝑖) ⊆ (‘suc 𝑖) → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))
124109, 112, 1233syl 18 . . . . . . . . . . . . . 14 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))
125108, 124anim12d 585 . . . . . . . . . . . . 13 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
12661, 68, 125syl2anc 692 . . . . . . . . . . . 12 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
127126ex 450 . . . . . . . . . . 11 (𝑖 ∈ ω → ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))))
1288, 16, 24, 58, 127finds2 7048 . . . . . . . . . 10 (𝑚 ∈ ω → ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚)))))
129128imp 445 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))))
130129simprd 479 . . . . . . . 8 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑗𝑚 → (𝑗) ⊆ (𝑚)))
131130expcom 451 . . . . . . 7 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → (𝑗𝑚 → (𝑗) ⊆ (𝑚))))
132131ralrimdv 2963 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → ∀𝑗𝑚 (𝑗) ⊆ (𝑚)))
133132ralrimiv 2960 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚))
134 frn 6015 . . . . . . . . . . . 12 (:ω⟶𝑆 → ran 𝑆)
135 ffun 6010 . . . . . . . . . . . . . . . 16 (𝑠:suc 𝑛𝐴 → Fun 𝑠)
1361353ad2ant1 1080 . . . . . . . . . . . . . . 15 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → Fun 𝑠)
137136rexlimivw 3023 . . . . . . . . . . . . . 14 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → Fun 𝑠)
138137ss2abi 3658 . . . . . . . . . . . . 13 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠}
13928, 138eqsstri 3619 . . . . . . . . . . . 12 𝑆 ⊆ {𝑠 ∣ Fun 𝑠}
140134, 139syl6ss 3599 . . . . . . . . . . 11 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ Fun 𝑠})
141140sseld 3586 . . . . . . . . . 10 (:ω⟶𝑆 → (𝑢 ∈ ran 𝑢 ∈ {𝑠 ∣ Fun 𝑠}))
142 vex 3192 . . . . . . . . . . 11 𝑢 ∈ V
143 funeq 5872 . . . . . . . . . . 11 (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢))
144142, 143elab 3337 . . . . . . . . . 10 (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢)
145141, 144syl6ib 241 . . . . . . . . 9 (:ω⟶𝑆 → (𝑢 ∈ ran → Fun 𝑢))
146145adantr 481 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → Fun 𝑢))
147 ffn 6007 . . . . . . . . 9 (:ω⟶𝑆 Fn ω)
148 fvelrnb 6205 . . . . . . . . . . . . 13 ( Fn ω → (𝑣 ∈ ran ↔ ∃𝑏 ∈ ω (𝑏) = 𝑣))
149 fvelrnb 6205 . . . . . . . . . . . . . . 15 ( Fn ω → (𝑢 ∈ ran ↔ ∃𝑎 ∈ ω (𝑎) = 𝑢))
150 nnord 7027 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ω → Ord 𝑎)
151 nnord 7027 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ ω → Ord 𝑏)
152150, 151anim12i 589 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord 𝑎 ∧ Ord 𝑏))
153 ordtri3or 5719 . . . . . . . . . . . . . . . . . . . . . . 23 ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎𝑏𝑎 = 𝑏𝑏𝑎))
154 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑏 → (𝑚) = (𝑏))
155154sseq2d 3617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑏 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑏)))
156155raleqbi1dv 3138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 = 𝑏 → (∀𝑗𝑚 (𝑗) ⊆ (𝑚) ↔ ∀𝑗𝑏 (𝑗) ⊆ (𝑏)))
157156rspcv 3294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ∀𝑗𝑏 (𝑗) ⊆ (𝑏)))
158 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑎 → (𝑗) = (𝑎))
159158sseq1d 3616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑎 → ((𝑗) ⊆ (𝑏) ↔ (𝑎) ⊆ (𝑏)))
160159rspccv 3295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑗𝑏 (𝑗) ⊆ (𝑏) → (𝑎𝑏 → (𝑎) ⊆ (𝑏)))
161157, 160syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → (𝑎) ⊆ (𝑏))))
162161adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → (𝑎) ⊆ (𝑏))))
1631623imp 1254 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑎𝑏) → (𝑎) ⊆ (𝑏))
164163orcd 407 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑎𝑏) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1651643exp 1261 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
166165com3r 87 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
167 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑏 → (𝑎) = (𝑏))
168 eqimss 3641 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎) = (𝑏) → (𝑎) ⊆ (𝑏))
169168orcd 407 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎) = (𝑏) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
170167, 169syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑏 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1711702a1d 26 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
172 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑎 → (𝑚) = (𝑎))
173172sseq2d 3617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑎 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑎)))
174173raleqbi1dv 3138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 = 𝑎 → (∀𝑗𝑚 (𝑗) ⊆ (𝑚) ↔ ∀𝑗𝑎 (𝑗) ⊆ (𝑎)))
175174rspcv 3294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ∀𝑗𝑎 (𝑗) ⊆ (𝑎)))
176 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑏 → (𝑗) = (𝑏))
177176sseq1d 3616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑏 → ((𝑗) ⊆ (𝑎) ↔ (𝑏) ⊆ (𝑎)))
178177rspccv 3295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑗𝑎 (𝑗) ⊆ (𝑎) → (𝑏𝑎 → (𝑏) ⊆ (𝑎)))
179175, 178syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → (𝑏) ⊆ (𝑎))))
180179adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → (𝑏) ⊆ (𝑎))))
1811803imp 1254 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑏𝑎) → (𝑏) ⊆ (𝑎))
182181olcd 408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑏𝑎) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1831823exp 1261 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
184183com3r 87 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
185166, 171, 1843jaoi 1388 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑏𝑎 = 𝑏𝑏𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
186153, 185syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord 𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
187152, 186mpcom 38 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎))))
188 sseq12 3612 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → ((𝑎) ⊆ (𝑏) ↔ 𝑢𝑣))
189 sseq12 3612 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑏) = 𝑣 ∧ (𝑎) = 𝑢) → ((𝑏) ⊆ (𝑎) ↔ 𝑣𝑢))
190189ancoms 469 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → ((𝑏) ⊆ (𝑎) ↔ 𝑣𝑢))
191188, 190orbi12d 745 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)) ↔ (𝑢𝑣𝑣𝑢)))
192191biimpcd 239 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (𝑢𝑣𝑣𝑢)))
193187, 192syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (𝑢𝑣𝑣𝑢))))
194193com23 86 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))
195194exp4b 631 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ω → (𝑏 ∈ ω → ((𝑎) = 𝑢 → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))))
196195com23 86 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ω → ((𝑎) = 𝑢 → (𝑏 ∈ ω → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))))
197196rexlimiv 3021 . . . . . . . . . . . . . . . 16 (∃𝑎 ∈ ω (𝑎) = 𝑢 → (𝑏 ∈ ω → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
198197rexlimdv 3024 . . . . . . . . . . . . . . 15 (∃𝑎 ∈ ω (𝑎) = 𝑢 → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))
199149, 198syl6bi 243 . . . . . . . . . . . . . 14 ( Fn ω → (𝑢 ∈ ran → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
200199com23 86 . . . . . . . . . . . . 13 ( Fn ω → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (𝑢 ∈ ran → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
201148, 200sylbid 230 . . . . . . . . . . . 12 ( Fn ω → (𝑣 ∈ ran → (𝑢 ∈ ran → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
202201com24 95 . . . . . . . . . . 11 ( Fn ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢 ∈ ran → (𝑣 ∈ ran → (𝑢𝑣𝑣𝑢)))))
203202imp 445 . . . . . . . . . 10 (( Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → (𝑣 ∈ ran → (𝑢𝑣𝑣𝑢))))
204203ralrimdv 2963 . . . . . . . . 9 (( Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
205147, 204sylan 488 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
206146, 205jcad 555 . . . . . . 7 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢))))
207206ralrimiv 2960 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → ∀𝑢 ∈ ran (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
208 fununi 5927 . . . . . 6 (∀𝑢 ∈ ran (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)) → Fun ran )
209207, 208syl 17 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → Fun ran )
210133, 209syldan 487 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → Fun ran )
211 vex 3192 . . . . . . . . 9 𝑚 ∈ V
212211eldm2 5287 . . . . . . . 8 (𝑚 ∈ dom ran ↔ ∃𝑢𝑚, 𝑢⟩ ∈ ran )
213 eluni2 4411 . . . . . . . . . 10 (⟨𝑚, 𝑢⟩ ∈ ran ↔ ∃𝑣 ∈ ran 𝑚, 𝑢⟩ ∈ 𝑣)
214211, 142opeldm 5293 . . . . . . . . . . . . . . 15 (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ dom 𝑣)
215214a1i 11 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ dom 𝑣))
216134, 44syl6ss 3599 . . . . . . . . . . . . . . 15 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
217 ssel 3581 . . . . . . . . . . . . . . . 16 (ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
218 vex 3192 . . . . . . . . . . . . . . . . . 18 𝑣 ∈ V
219 dmeq 5289 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣)
220219eleq2d 2684 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣))
221219eleq1d 2683 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω))
222220, 221anbi12d 746 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
223218, 222elab 3337 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))
224223simprbi 480 . . . . . . . . . . . . . . . 16 (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → dom 𝑣 ∈ ω)
225217, 224syl6 35 . . . . . . . . . . . . . . 15 (ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran → dom 𝑣 ∈ ω))
226216, 225syl 17 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (𝑣 ∈ ran → dom 𝑣 ∈ ω))
227215, 226anim12d 585 . . . . . . . . . . . . 13 (:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣𝑣 ∈ ran ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
228 elnn 7029 . . . . . . . . . . . . 13 ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω)
229227, 228syl6 35 . . . . . . . . . . . 12 (:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣𝑣 ∈ ran ) → 𝑚 ∈ ω))
230229expcomd 454 . . . . . . . . . . 11 (:ω⟶𝑆 → (𝑣 ∈ ran → (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ ω)))
231230rexlimdv 3024 . . . . . . . . . 10 (:ω⟶𝑆 → (∃𝑣 ∈ ran 𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ ω))
232213, 231syl5bi 232 . . . . . . . . 9 (:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ ran 𝑚 ∈ ω))
233232exlimdv 1858 . . . . . . . 8 (:ω⟶𝑆 → (∃𝑢𝑚, 𝑢⟩ ∈ ran 𝑚 ∈ ω))
234212, 233syl5bi 232 . . . . . . 7 (:ω⟶𝑆 → (𝑚 ∈ dom ran 𝑚 ∈ ω))
235234adantr 481 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom ran 𝑚 ∈ ω))
236 id 22 . . . . . . . . . . 11 (𝑚 ∈ ω → 𝑚 ∈ ω)
237 fnfvelrn 6317 . . . . . . . . . . 11 (( Fn ω ∧ 𝑚 ∈ ω) → (𝑚) ∈ ran )
238147, 236, 237syl2anr 495 . . . . . . . . . 10 ((𝑚 ∈ ω ∧ :ω⟶𝑆) → (𝑚) ∈ ran )
239238adantrr 752 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑚) ∈ ran )
240129simpld 475 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 ∈ dom (𝑚))
241 dmeq 5289 . . . . . . . . . 10 (𝑢 = (𝑚) → dom 𝑢 = dom (𝑚))
242241eliuni 4497 . . . . . . . . 9 (((𝑚) ∈ ran 𝑚 ∈ dom (𝑚)) → 𝑚 𝑢 ∈ ran dom 𝑢)
243239, 240, 242syl2anc 692 . . . . . . . 8 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 𝑢 ∈ ran dom 𝑢)
244 dmuni 5299 . . . . . . . 8 dom ran = 𝑢 ∈ ran dom 𝑢
245243, 244syl6eleqr 2709 . . . . . . 7 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 ∈ dom ran )
246245expcom 451 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ran ))
247235, 246impbid 202 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom ran 𝑚 ∈ ω))
248247eqrdv 2619 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → dom ran = ω)
249 rnuni 5508 . . . . . 6 ran ran = 𝑠 ∈ ran ran 𝑠
250 frn 6015 . . . . . . . . . . . . . 14 (𝑠:suc 𝑛𝐴 → ran 𝑠𝐴)
2512503ad2ant1 1080 . . . . . . . . . . . . 13 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → ran 𝑠𝐴)
252251rexlimivw 3023 . . . . . . . . . . . 12 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → ran 𝑠𝐴)
253252ss2abi 3658 . . . . . . . . . . 11 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ ran 𝑠𝐴}
25428, 253eqsstri 3619 . . . . . . . . . 10 𝑆 ⊆ {𝑠 ∣ ran 𝑠𝐴}
255134, 254syl6ss 3599 . . . . . . . . 9 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ ran 𝑠𝐴})
256 ssel 3581 . . . . . . . . . 10 (ran ⊆ {𝑠 ∣ ran 𝑠𝐴} → (𝑠 ∈ ran 𝑠 ∈ {𝑠 ∣ ran 𝑠𝐴}))
257 abid 2609 . . . . . . . . . 10 (𝑠 ∈ {𝑠 ∣ ran 𝑠𝐴} ↔ ran 𝑠𝐴)
258256, 257syl6ib 241 . . . . . . . . 9 (ran ⊆ {𝑠 ∣ ran 𝑠𝐴} → (𝑠 ∈ ran → ran 𝑠𝐴))
259255, 258syl 17 . . . . . . . 8 (:ω⟶𝑆 → (𝑠 ∈ ran → ran 𝑠𝐴))
260259ralrimiv 2960 . . . . . . 7 (:ω⟶𝑆 → ∀𝑠 ∈ ran ran 𝑠𝐴)
261 iunss 4532 . . . . . . 7 ( 𝑠 ∈ ran ran 𝑠𝐴 ↔ ∀𝑠 ∈ ran ran 𝑠𝐴)
262260, 261sylibr 224 . . . . . 6 (:ω⟶𝑆 𝑠 ∈ ran ran 𝑠𝐴)
263249, 262syl5eqss 3633 . . . . 5 (:ω⟶𝑆 → ran ran 𝐴)
264263adantr 481 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ran ran 𝐴)
265 df-fn 5855 . . . . 5 ( ran Fn ω ↔ (Fun ran ∧ dom ran = ω))
266 df-f 5856 . . . . . 6 ( ran :ω⟶𝐴 ↔ ( ran Fn ω ∧ ran ran 𝐴))
267266biimpri 218 . . . . 5 (( ran Fn ω ∧ ran ran 𝐴) → ran :ω⟶𝐴)
268265, 267sylanbr 490 . . . 4 (((Fun ran ∧ dom ran = ω) ∧ ran ran 𝐴) → ran :ω⟶𝐴)
269210, 248, 264, 268syl21anc 1322 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ran :ω⟶𝐴)
270 fnfvelrn 6317 . . . . . . . 8 (( Fn ω ∧ ∅ ∈ ω) → (‘∅) ∈ ran )
271147, 25, 270sylancl 693 . . . . . . 7 (:ω⟶𝑆 → (‘∅) ∈ ran )
272271adantr 481 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘∅) ∈ ran )
273 elssuni 4438 . . . . . 6 ((‘∅) ∈ ran → (‘∅) ⊆ ran )
274272, 273syl 17 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘∅) ⊆ ran )
27554adantr 481 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∅ ∈ dom (‘∅))
276 funssfv 6171 . . . . 5 ((Fun ran ∧ (‘∅) ⊆ ran ∧ ∅ ∈ dom (‘∅)) → ( ran ‘∅) = ((‘∅)‘∅))
277210, 274, 275, 276syl3anc 1323 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ( ran ‘∅) = ((‘∅)‘∅))
278 simp2 1060 . . . . . . . . . . 11 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑠‘∅) = 𝐶)
279278rexlimivw 3023 . . . . . . . . . 10 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑠‘∅) = 𝐶)
280279ss2abi 3658 . . . . . . . . 9 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
28128, 280eqsstri 3619 . . . . . . . 8 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
282134, 281syl6ss 3599 . . . . . . 7 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶})
283 ssel 3581 . . . . . . . 8 (ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((‘∅) ∈ ran → (‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶}))
284 fveq1 6152 . . . . . . . . . 10 (𝑠 = (‘∅) → (𝑠‘∅) = ((‘∅)‘∅))
285284eqeq1d 2623 . . . . . . . . 9 (𝑠 = (‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((‘∅)‘∅) = 𝐶))
28646, 285elab 3337 . . . . . . . 8 ((‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((‘∅)‘∅) = 𝐶)
287283, 286syl6ib 241 . . . . . . 7 (ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
288282, 287syl 17 . . . . . 6 (:ω⟶𝑆 → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
289288adantr 481 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
290272, 289mpd 15 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((‘∅)‘∅) = 𝐶)
291277, 290eqtrd 2655 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ( ran ‘∅) = 𝐶)
292 nfv 1840 . . . . 5 𝑘 :ω⟶𝑆
293 nfra1 2936 . . . . 5 𝑘𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))
294292, 293nfan 1825 . . . 4 𝑘(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))
295134ad2antrr 761 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ran 𝑆)
296 peano2 7040 . . . . . . . . 9 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
297 fnfvelrn 6317 . . . . . . . . 9 (( Fn ω ∧ suc 𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
298147, 296, 297syl2an 494 . . . . . . . 8 ((:ω⟶𝑆𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
299298adantlr 750 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
300240expcom 451 . . . . . . . . 9 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (𝑚)))
301300ralrimiv 2960 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚))
302 id 22 . . . . . . . . . . 11 (𝑚 = suc 𝑘𝑚 = suc 𝑘)
303 fveq2 6153 . . . . . . . . . . . 12 (𝑚 = suc 𝑘 → (𝑚) = (‘suc 𝑘))
304303dmeqd 5291 . . . . . . . . . . 11 (𝑚 = suc 𝑘 → dom (𝑚) = dom (‘suc 𝑘))
305302, 304eleq12d 2692 . . . . . . . . . 10 (𝑚 = suc 𝑘 → (𝑚 ∈ dom (𝑚) ↔ suc 𝑘 ∈ dom (‘suc 𝑘)))
306305rspcv 3294 . . . . . . . . 9 (suc 𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚) → suc 𝑘 ∈ dom (‘suc 𝑘)))
307296, 306syl 17 . . . . . . . 8 (𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚) → suc 𝑘 ∈ dom (‘suc 𝑘)))
308301, 307mpan9 486 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (‘suc 𝑘))
309 eleq2 2687 . . . . . . . . . . . . . . . . . . . . 21 (dom 𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛))
310309biimpa 501 . . . . . . . . . . . . . . . . . . . 20 ((dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
31129, 310sylan 488 . . . . . . . . . . . . . . . . . . 19 ((𝑠:suc 𝑛𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
312 ordsucelsuc 6976 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord 𝑛 → (𝑘𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
31330, 312syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ω → (𝑘𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
314313biimprd 238 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛𝑘𝑛))
315 rsp 2924 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑘𝑛 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))
316314, 315syl9r 78 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
317316com13 88 . . . . . . . . . . . . . . . . . . 19 (suc 𝑘 ∈ suc 𝑛 → (𝑛 ∈ ω → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
318311, 317syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑠:suc 𝑛𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → (𝑛 ∈ ω → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
319318ex 450 . . . . . . . . . . . . . . . . 17 (𝑠:suc 𝑛𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))))
320319com24 95 . . . . . . . . . . . . . . . 16 (𝑠:suc 𝑛𝐴 → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))))
321320imp 445 . . . . . . . . . . . . . . 15 ((𝑠:suc 𝑛𝐴 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
3223213adant2 1078 . . . . . . . . . . . . . 14 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
323322impcom 446 . . . . . . . . . . . . 13 ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))
324323rexlimiva 3022 . . . . . . . . . . . 12 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))
325324ss2abi 3658 . . . . . . . . . . 11 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
32628, 325eqsstri 3619 . . . . . . . . . 10 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
327 sstr 3595 . . . . . . . . . 10 ((ran 𝑆𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}) → ran ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))})
328326, 327mpan2 706 . . . . . . . . 9 (ran 𝑆 → ran ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))})
329328sseld 3586 . . . . . . . 8 (ran 𝑆 → ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}))
330 fvex 6163 . . . . . . . . 9 (‘suc 𝑘) ∈ V
331 dmeq 5289 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → dom 𝑠 = dom (‘suc 𝑘))
332331eleq2d 2684 . . . . . . . . . 10 (𝑠 = (‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (‘suc 𝑘)))
333 fveq1 6152 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → (𝑠‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
334 fveq1 6152 . . . . . . . . . . . 12 (𝑠 = (‘suc 𝑘) → (𝑠𝑘) = ((‘suc 𝑘)‘𝑘))
335334fveq2d 6157 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → (𝐹‘(𝑠𝑘)) = (𝐹‘((‘suc 𝑘)‘𝑘)))
336333, 335eleq12d 2692 . . . . . . . . . 10 (𝑠 = (‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) ↔ ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
337332, 336imbi12d 334 . . . . . . . . 9 (𝑠 = (‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) ↔ (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))))
338330, 337elab 3337 . . . . . . . 8 ((‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ↔ (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
339329, 338syl6ib 241 . . . . . . 7 (ran 𝑆 → ((‘suc 𝑘) ∈ ran → (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))))
340295, 299, 308, 339syl3c 66 . . . . . 6 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))
341210adantr 481 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → Fun ran )
342 elssuni 4438 . . . . . . . . . 10 ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ⊆ ran )
343298, 342syl 17 . . . . . . . . 9 ((:ω⟶𝑆𝑘 ∈ ω) → (‘suc 𝑘) ⊆ ran )
344343adantlr 750 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ⊆ ran )
345 funssfv 6171 . . . . . . . 8 ((Fun ran ∧ (‘suc 𝑘) ⊆ ran ∧ suc 𝑘 ∈ dom (‘suc 𝑘)) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
346341, 344, 308, 345syl3anc 1323 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
347216sseld 3586 . . . . . . . . . . . . . . 15 (:ω⟶𝑆 → ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
348331eleq2d 2684 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (‘suc 𝑘)))
349331eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (‘suc 𝑘) ∈ ω))
350348, 349anbi12d 746 . . . . . . . . . . . . . . . 16 (𝑠 = (‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
351330, 350elab 3337 . . . . . . . . . . . . . . 15 ((‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω))
352347, 351syl6ib 241 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → ((‘suc 𝑘) ∈ ran → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
353352adantr 481 . . . . . . . . . . . . 13 ((:ω⟶𝑆𝑘 ∈ ω) → ((‘suc 𝑘) ∈ ran → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
354298, 353mpd 15 . . . . . . . . . . . 12 ((:ω⟶𝑆𝑘 ∈ ω) → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω))
355354simprd 479 . . . . . . . . . . 11 ((:ω⟶𝑆𝑘 ∈ ω) → dom (‘suc 𝑘) ∈ ω)
356 nnord 7027 . . . . . . . . . . 11 (dom (‘suc 𝑘) ∈ ω → Ord dom (‘suc 𝑘))
357 ordtr 5701 . . . . . . . . . . 11 (Ord dom (‘suc 𝑘) → Tr dom (‘suc 𝑘))
358 trsuc 5774 . . . . . . . . . . . 12 ((Tr dom (‘suc 𝑘) ∧ suc 𝑘 ∈ dom (‘suc 𝑘)) → 𝑘 ∈ dom (‘suc 𝑘))
359358ex 450 . . . . . . . . . . 11 (Tr dom (‘suc 𝑘) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
360355, 356, 357, 3594syl 19 . . . . . . . . . 10 ((:ω⟶𝑆𝑘 ∈ ω) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
361360adantlr 750 . . . . . . . . 9 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
362308, 361mpd 15 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom (‘suc 𝑘))
363 funssfv 6171 . . . . . . . 8 ((Fun ran ∧ (‘suc 𝑘) ⊆ ran 𝑘 ∈ dom (‘suc 𝑘)) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
364341, 344, 362, 363syl3anc 1323 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
365 simpl 473 . . . . . . . 8 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
366 simpr 477 . . . . . . . . 9 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
367366fveq2d 6157 . . . . . . . 8 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → (𝐹‘( ran 𝑘)) = (𝐹‘((‘suc 𝑘)‘𝑘)))
368365, 367eleq12d 2692 . . . . . . 7 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → (( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)) ↔ ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
369346, 364, 368syl2anc 692 . . . . . 6 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)) ↔ ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
370340, 369mpbird 247 . . . . 5 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))
371370ex 450 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑘 ∈ ω → ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
372294, 371ralrimi 2952 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))
373 vex 3192 . . . . . 6 ∈ V
374373rnex 7054 . . . . 5 ran ∈ V
375374uniex 6913 . . . 4 ran ∈ V
376 feq1 5988 . . . . 5 (𝑔 = ran → (𝑔:ω⟶𝐴 ran :ω⟶𝐴))
377 fveq1 6152 . . . . . 6 (𝑔 = ran → (𝑔‘∅) = ( ran ‘∅))
378377eqeq1d 2623 . . . . 5 (𝑔 = ran → ((𝑔‘∅) = 𝐶 ↔ ( ran ‘∅) = 𝐶))
379 fveq1 6152 . . . . . . 7 (𝑔 = ran → (𝑔‘suc 𝑘) = ( ran ‘suc 𝑘))
380 fveq1 6152 . . . . . . . 8 (𝑔 = ran → (𝑔𝑘) = ( ran 𝑘))
381380fveq2d 6157 . . . . . . 7 (𝑔 = ran → (𝐹‘(𝑔𝑘)) = (𝐹‘( ran 𝑘)))
382379, 381eleq12d 2692 . . . . . 6 (𝑔 = ran → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
383382ralbidv 2981 . . . . 5 (𝑔 = ran → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
384376, 378, 3833anbi123d 1396 . . . 4 (𝑔 = ran → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))) ↔ ( ran :ω⟶𝐴 ∧ ( ran ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))))
385375, 384spcev 3289 . . 3 (( ran :ω⟶𝐴 ∧ ( ran ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
386269, 291, 372, 385syl3anc 1323 . 2 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
387386exlimiv 1855 1 (∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3o 1035  w3a 1036   = wceq 1480  wex 1701  wcel 1987  {cab 2607  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  wss 3559  c0 3896  cop 4159   cuni 4407   ciun 4490  cmpt 4678  Tr wtr 4717  dom cdm 5079  ran crn 5080  cres 5081  Ord word 5686  suc csuc 5689  Fun wfun 5846   Fn wfn 5847  wf 5848  cfv 5852  ωcom 7019
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-dc 9220
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-fv 5860  df-om 7020  df-1o 7512
This theorem is referenced by:  axdc3lem4  9227
  Copyright terms: Public domain W3C validator