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

Theorem axdc3lem2 10491
Description: Lemma for axdc3 10494. 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 10486 (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 10486 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 6906 . . . . . . . . . . . . . 14 (𝑚 = ∅ → (𝑚) = (‘∅))
32dmeqd 5916 . . . . . . . . . . . . 13 (𝑚 = ∅ → dom (𝑚) = dom (‘∅))
41, 3eleq12d 2835 . . . . . . . . . . . 12 (𝑚 = ∅ → (𝑚 ∈ dom (𝑚) ↔ ∅ ∈ dom (‘∅)))
5 eleq2 2830 . . . . . . . . . . . . 13 (𝑚 = ∅ → (𝑗𝑚𝑗 ∈ ∅))
62sseq2d 4016 . . . . . . . . . . . . 13 (𝑚 = ∅ → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (‘∅)))
75, 6imbi12d 344 . . . . . . . . . . . 12 (𝑚 = ∅ → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
84, 7anbi12d 632 . . . . . . . . . . 11 (𝑚 = ∅ → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅)))))
9 id 22 . . . . . . . . . . . . 13 (𝑚 = 𝑖𝑚 = 𝑖)
10 fveq2 6906 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → (𝑚) = (𝑖))
1110dmeqd 5916 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → dom (𝑚) = dom (𝑖))
129, 11eleq12d 2835 . . . . . . . . . . . 12 (𝑚 = 𝑖 → (𝑚 ∈ dom (𝑚) ↔ 𝑖 ∈ dom (𝑖)))
13 elequ2 2123 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → (𝑗𝑚𝑗𝑖))
1410sseq2d 4016 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑖)))
1513, 14imbi12d 344 . . . . . . . . . . . 12 (𝑚 = 𝑖 → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗𝑖 → (𝑗) ⊆ (𝑖))))
1612, 15anbi12d 632 . . . . . . . . . . 11 (𝑚 = 𝑖 → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖)))))
17 id 22 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖𝑚 = suc 𝑖)
18 fveq2 6906 . . . . . . . . . . . . . 14 (𝑚 = suc 𝑖 → (𝑚) = (‘suc 𝑖))
1918dmeqd 5916 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → dom (𝑚) = dom (‘suc 𝑖))
2017, 19eleq12d 2835 . . . . . . . . . . . 12 (𝑚 = suc 𝑖 → (𝑚 ∈ dom (𝑚) ↔ suc 𝑖 ∈ dom (‘suc 𝑖)))
21 eleq2 2830 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → (𝑗𝑚𝑗 ∈ suc 𝑖))
2218sseq2d 4016 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (‘suc 𝑖)))
2321, 22imbi12d 344 . . . . . . . . . . . 12 (𝑚 = suc 𝑖 → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))
2420, 23anbi12d 632 . . . . . . . . . . 11 (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
25 peano1 7910 . . . . . . . . . . . . . . 15 ∅ ∈ ω
26 ffvelcdm 7101 . . . . . . . . . . . . . . 15 ((:ω⟶𝑆 ∧ ∅ ∈ ω) → (‘∅) ∈ 𝑆)
2725, 26mpan2 691 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (‘∅) ∈ 𝑆)
28 axdc3lem2.2 . . . . . . . . . . . . . . . . . 18 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
29 fdm 6745 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠:suc 𝑛𝐴 → dom 𝑠 = suc 𝑛)
30 nnord 7895 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ω → Ord 𝑛)
31 0elsuc 7855 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝑛 → ∅ ∈ suc 𝑛)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → ∅ ∈ suc 𝑛)
33 peano2 7912 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
34 eleq2 2830 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛))
35 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω))
3634, 35anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom 𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω)))
3736biimprcd 250 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
3832, 33, 37syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ω → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
3929, 38syl5com 31 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠:suc 𝑛𝐴 → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
40393ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
4140impcom 407 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
4241rexlimiva 3147 . . . . . . . . . . . . . . . . . . 19 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
4342ss2abi 4067 . . . . . . . . . . . . . . . . . 18 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
4428, 43eqsstri 4030 . . . . . . . . . . . . . . . . 17 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
4544sseli 3979 . . . . . . . . . . . . . . . 16 ((‘∅) ∈ 𝑆 → (‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
46 fvex 6919 . . . . . . . . . . . . . . . . 17 (‘∅) ∈ V
47 dmeq 5914 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (‘∅) → dom 𝑠 = dom (‘∅))
4847eleq2d 2827 . . . . . . . . . . . . . . . . . 18 (𝑠 = (‘∅) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (‘∅)))
4947eleq1d 2826 . . . . . . . . . . . . . . . . . 18 (𝑠 = (‘∅) → (dom 𝑠 ∈ ω ↔ dom (‘∅) ∈ ω))
5048, 49anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘∅) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω)))
5146, 50elab 3679 . . . . . . . . . . . . . . . 16 ((‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω))
5245, 51sylib 218 . . . . . . . . . . . . . . 15 ((‘∅) ∈ 𝑆 → (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω))
5352simpld 494 . . . . . . . . . . . . . 14 ((‘∅) ∈ 𝑆 → ∅ ∈ dom (‘∅))
5427, 53syl 17 . . . . . . . . . . . . 13 (:ω⟶𝑆 → ∅ ∈ dom (‘∅))
55 noel 4338 . . . . . . . . . . . . . 14 ¬ 𝑗 ∈ ∅
5655pm2.21i 119 . . . . . . . . . . . . 13 (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))
5754, 56jctir 520 . . . . . . . . . . . 12 (:ω⟶𝑆 → (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
5857adantr 480 . . . . . . . . . . 11 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
59 ffvelcdm 7101 . . . . . . . . . . . . . . 15 ((:ω⟶𝑆𝑖 ∈ ω) → (𝑖) ∈ 𝑆)
6059ancoms 458 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ :ω⟶𝑆) → (𝑖) ∈ 𝑆)
6160adantrr 717 . . . . . . . . . . . . 13 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑖) ∈ 𝑆)
62 suceq 6450 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
6362fveq2d 6910 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (‘suc 𝑘) = (‘suc 𝑖))
64 2fveq3 6911 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (𝐺‘(𝑘)) = (𝐺‘(𝑖)))
6563, 64eleq12d 2835 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((‘suc 𝑘) ∈ (𝐺‘(𝑘)) ↔ (‘suc 𝑖) ∈ (𝐺‘(𝑖))))
6665rspcva 3620 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘suc 𝑖) ∈ (𝐺‘(𝑖)))
6766adantrl 716 . . . . . . . . . . . . 13 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (‘suc 𝑖) ∈ (𝐺‘(𝑖)))
6844sseli 3979 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ 𝑆 → (𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
69 fvex 6919 . . . . . . . . . . . . . . . . . . . . 21 (𝑖) ∈ V
70 dmeq 5914 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑖) → dom 𝑠 = dom (𝑖))
7170eleq2d 2827 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (𝑖)))
7270eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑖) → (dom 𝑠 ∈ ω ↔ dom (𝑖) ∈ ω))
7371, 72anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω)))
7469, 73elab 3679 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω))
7568, 74sylib 218 . . . . . . . . . . . . . . . . . . 19 ((𝑖) ∈ 𝑆 → (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω))
7675simprd 495 . . . . . . . . . . . . . . . . . 18 ((𝑖) ∈ 𝑆 → dom (𝑖) ∈ ω)
77 nnord 7895 . . . . . . . . . . . . . . . . . 18 (dom (𝑖) ∈ ω → Ord dom (𝑖))
78 ordsucelsuc 7842 . . . . . . . . . . . . . . . . . 18 (Ord dom (𝑖) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
7976, 77, 783syl 18 . . . . . . . . . . . . . . . . 17 ((𝑖) ∈ 𝑆 → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
8079adantr 480 . . . . . . . . . . . . . . . 16 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
81 dmeq 5914 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑖) → dom 𝑥 = dom (𝑖))
82 suceq 6450 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑥 = dom (𝑖) → suc dom 𝑥 = suc dom (𝑖))
8381, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → suc dom 𝑥 = suc dom (𝑖))
8483eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (𝑖)))
8581reseq2d 5997 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (𝑖)))
86 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → 𝑥 = (𝑖))
8785, 86eqeq12d 2753 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (𝑖)) = (𝑖)))
8884, 87anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑖) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))))
8988rabbidv 3444 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑖) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))})
90 axdc3lem2.3 . . . . . . . . . . . . . . . . . . . . . 22 𝐺 = (𝑥𝑆 ↦ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
91 axdc3lem2.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝐴 ∈ V
9291, 28axdc3lem 10490 . . . . . . . . . . . . . . . . . . . . . . 23 𝑆 ∈ V
9392rabex 5339 . . . . . . . . . . . . . . . . . . . . . 22 {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))} ∈ V
9489, 90, 93fvmpt 7016 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖) ∈ 𝑆 → (𝐺‘(𝑖)) = {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))})
9594eleq2d 2827 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ 𝑆 → ((‘suc 𝑖) ∈ (𝐺‘(𝑖)) ↔ (‘suc 𝑖) ∈ {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))}))
96 dmeq 5914 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (‘suc 𝑖) → dom 𝑦 = dom (‘suc 𝑖))
9796eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (‘suc 𝑖) → (dom 𝑦 = suc dom (𝑖) ↔ dom (‘suc 𝑖) = suc dom (𝑖)))
98 reseq1 5991 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (‘suc 𝑖) → (𝑦 ↾ dom (𝑖)) = ((‘suc 𝑖) ↾ dom (𝑖)))
9998eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (‘suc 𝑖) → ((𝑦 ↾ dom (𝑖)) = (𝑖) ↔ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))
10097, 99anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (‘suc 𝑖) → ((dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖)) ↔ (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖))))
101100elrab 3692 . . . . . . . . . . . . . . . . . . . 20 ((‘suc 𝑖) ∈ {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))} ↔ ((‘suc 𝑖) ∈ 𝑆 ∧ (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖))))
10295, 101bitrdi 287 . . . . . . . . . . . . . . . . . . 19 ((𝑖) ∈ 𝑆 → ((‘suc 𝑖) ∈ (𝐺‘(𝑖)) ↔ ((‘suc 𝑖) ∈ 𝑆 ∧ (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))))
103102simplbda 499 . . . . . . . . . . . . . . . . . 18 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))
104103simpld 494 . . . . . . . . . . . . . . . . 17 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → dom (‘suc 𝑖) = suc dom (𝑖))
105104eleq2d 2827 . . . . . . . . . . . . . . . 16 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
10680, 105bitr4d 282 . . . . . . . . . . . . . . 15 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ dom (‘suc 𝑖)))
107106biimpd 229 . . . . . . . . . . . . . 14 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) → suc 𝑖 ∈ dom (‘suc 𝑖)))
108103simprd 495 . . . . . . . . . . . . . . 15 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖))
109 resss 6019 . . . . . . . . . . . . . . . 16 ((‘suc 𝑖) ↾ dom (𝑖)) ⊆ (‘suc 𝑖)
110 sseq1 4009 . . . . . . . . . . . . . . . 16 (((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖) → (((‘suc 𝑖) ↾ dom (𝑖)) ⊆ (‘suc 𝑖) ↔ (𝑖) ⊆ (‘suc 𝑖)))
111109, 110mpbii 233 . . . . . . . . . . . . . . 15 (((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖) → (𝑖) ⊆ (‘suc 𝑖))
112 elsuci 6451 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ suc 𝑖 → (𝑗𝑖𝑗 = 𝑖))
113 pm2.27 42 . . . . . . . . . . . . . . . . . . 19 (𝑗𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → (𝑗) ⊆ (𝑖)))
114 sstr2 3990 . . . . . . . . . . . . . . . . . . 19 ((𝑗) ⊆ (𝑖) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖)))
115113, 114syl6 35 . . . . . . . . . . . . . . . . . 18 (𝑗𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
116 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝑗) = (𝑖))
117116sseq1d 4015 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → ((𝑗) ⊆ (‘suc 𝑖) ↔ (𝑖) ⊆ (‘suc 𝑖)))
118117biimprd 248 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖)))
119118a1d 25 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
120115, 119jaoi 858 . . . . . . . . . . . . . . . . 17 ((𝑗𝑖𝑗 = 𝑖) → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
121112, 120syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ suc 𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
122121com13 88 . . . . . . . . . . . . . . 15 ((𝑖) ⊆ (‘suc 𝑖) → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))
123108, 111, 1223syl 18 . . . . . . . . . . . . . 14 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))
124107, 123anim12d 609 . . . . . . . . . . . . 13 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
12561, 67, 124syl2anc 584 . . . . . . . . . . . 12 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
126125ex 412 . . . . . . . . . . 11 (𝑖 ∈ ω → ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))))
1278, 16, 24, 58, 126finds2 7920 . . . . . . . . . 10 (𝑚 ∈ ω → ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚)))))
128127imp 406 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))))
129128simprd 495 . . . . . . . 8 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑗𝑚 → (𝑗) ⊆ (𝑚)))
130129expcom 413 . . . . . . 7 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → (𝑗𝑚 → (𝑗) ⊆ (𝑚))))
131130ralrimdv 3152 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → ∀𝑗𝑚 (𝑗) ⊆ (𝑚)))
132131ralrimiv 3145 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚))
133 frn 6743 . . . . . . . . . . . 12 (:ω⟶𝑆 → ran 𝑆)
134 ffun 6739 . . . . . . . . . . . . . . . 16 (𝑠:suc 𝑛𝐴 → Fun 𝑠)
1351343ad2ant1 1134 . . . . . . . . . . . . . . 15 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → Fun 𝑠)
136135rexlimivw 3151 . . . . . . . . . . . . . 14 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → Fun 𝑠)
137136ss2abi 4067 . . . . . . . . . . . . 13 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠}
13828, 137eqsstri 4030 . . . . . . . . . . . 12 𝑆 ⊆ {𝑠 ∣ Fun 𝑠}
139133, 138sstrdi 3996 . . . . . . . . . . 11 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ Fun 𝑠})
140139sseld 3982 . . . . . . . . . 10 (:ω⟶𝑆 → (𝑢 ∈ ran 𝑢 ∈ {𝑠 ∣ Fun 𝑠}))
141 vex 3484 . . . . . . . . . . 11 𝑢 ∈ V
142 funeq 6586 . . . . . . . . . . 11 (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢))
143141, 142elab 3679 . . . . . . . . . 10 (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢)
144140, 143imbitrdi 251 . . . . . . . . 9 (:ω⟶𝑆 → (𝑢 ∈ ran → Fun 𝑢))
145144adantr 480 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → Fun 𝑢))
146 ffn 6736 . . . . . . . . 9 (:ω⟶𝑆 Fn ω)
147 fvelrnb 6969 . . . . . . . . . . . . 13 ( Fn ω → (𝑣 ∈ ran ↔ ∃𝑏 ∈ ω (𝑏) = 𝑣))
148 fvelrnb 6969 . . . . . . . . . . . . . . 15 ( Fn ω → (𝑢 ∈ ran ↔ ∃𝑎 ∈ ω (𝑎) = 𝑢))
149 nnord 7895 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ω → Ord 𝑎)
150 nnord 7895 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ ω → Ord 𝑏)
151149, 150anim12i 613 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord 𝑎 ∧ Ord 𝑏))
152 ordtri3or 6416 . . . . . . . . . . . . . . . . . . . . . . 23 ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎𝑏𝑎 = 𝑏𝑏𝑎))
153 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑏 → (𝑚) = (𝑏))
154153sseq2d 4016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑏 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑏)))
155154raleqbi1dv 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 = 𝑏 → (∀𝑗𝑚 (𝑗) ⊆ (𝑚) ↔ ∀𝑗𝑏 (𝑗) ⊆ (𝑏)))
156155rspcv 3618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ∀𝑗𝑏 (𝑗) ⊆ (𝑏)))
157 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑎 → (𝑗) = (𝑎))
158157sseq1d 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑎 → ((𝑗) ⊆ (𝑏) ↔ (𝑎) ⊆ (𝑏)))
159158rspccv 3619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑗𝑏 (𝑗) ⊆ (𝑏) → (𝑎𝑏 → (𝑎) ⊆ (𝑏)))
160156, 159syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → (𝑎) ⊆ (𝑏))))
161160adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → (𝑎) ⊆ (𝑏))))
1621613imp 1111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑎𝑏) → (𝑎) ⊆ (𝑏))
163162orcd 874 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑎𝑏) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1641633exp 1120 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
165164com3r 87 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
166 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑏 → (𝑎) = (𝑏))
167 eqimss 4042 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎) = (𝑏) → (𝑎) ⊆ (𝑏))
168167orcd 874 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎) = (𝑏) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
169166, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑏 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1701692a1d 26 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
171 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑎 → (𝑚) = (𝑎))
172171sseq2d 4016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑎 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑎)))
173172raleqbi1dv 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 = 𝑎 → (∀𝑗𝑚 (𝑗) ⊆ (𝑚) ↔ ∀𝑗𝑎 (𝑗) ⊆ (𝑎)))
174173rspcv 3618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ∀𝑗𝑎 (𝑗) ⊆ (𝑎)))
175 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑏 → (𝑗) = (𝑏))
176175sseq1d 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑏 → ((𝑗) ⊆ (𝑎) ↔ (𝑏) ⊆ (𝑎)))
177176rspccv 3619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑗𝑎 (𝑗) ⊆ (𝑎) → (𝑏𝑎 → (𝑏) ⊆ (𝑎)))
178174, 177syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → (𝑏) ⊆ (𝑎))))
179178adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → (𝑏) ⊆ (𝑎))))
1801793imp 1111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑏𝑎) → (𝑏) ⊆ (𝑎))
181180olcd 875 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑏𝑎) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1821813exp 1120 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
183182com3r 87 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
184165, 170, 1833jaoi 1430 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑏𝑎 = 𝑏𝑏𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
185152, 184syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord 𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
186151, 185mpcom 38 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎))))
187 sseq12 4011 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → ((𝑎) ⊆ (𝑏) ↔ 𝑢𝑣))
188 sseq12 4011 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑏) = 𝑣 ∧ (𝑎) = 𝑢) → ((𝑏) ⊆ (𝑎) ↔ 𝑣𝑢))
189188ancoms 458 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → ((𝑏) ⊆ (𝑎) ↔ 𝑣𝑢))
190187, 189orbi12d 919 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)) ↔ (𝑢𝑣𝑣𝑢)))
191190biimpcd 249 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (𝑢𝑣𝑣𝑢)))
192186, 191syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (𝑢𝑣𝑣𝑢))))
193192com23 86 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))
194193exp4b 430 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ω → (𝑏 ∈ ω → ((𝑎) = 𝑢 → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))))
195194com23 86 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ω → ((𝑎) = 𝑢 → (𝑏 ∈ ω → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))))
196195rexlimiv 3148 . . . . . . . . . . . . . . . 16 (∃𝑎 ∈ ω (𝑎) = 𝑢 → (𝑏 ∈ ω → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
197196rexlimdv 3153 . . . . . . . . . . . . . . 15 (∃𝑎 ∈ ω (𝑎) = 𝑢 → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))
198148, 197biimtrdi 253 . . . . . . . . . . . . . 14 ( Fn ω → (𝑢 ∈ ran → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
199198com23 86 . . . . . . . . . . . . 13 ( Fn ω → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (𝑢 ∈ ran → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
200147, 199sylbid 240 . . . . . . . . . . . 12 ( Fn ω → (𝑣 ∈ ran → (𝑢 ∈ ran → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
201200com24 95 . . . . . . . . . . 11 ( Fn ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢 ∈ ran → (𝑣 ∈ ran → (𝑢𝑣𝑣𝑢)))))
202201imp 406 . . . . . . . . . 10 (( Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → (𝑣 ∈ ran → (𝑢𝑣𝑣𝑢))))
203202ralrimdv 3152 . . . . . . . . 9 (( Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
204146, 203sylan 580 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
205145, 204jcad 512 . . . . . . 7 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢))))
206205ralrimiv 3145 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → ∀𝑢 ∈ ran (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
207 fununi 6641 . . . . . 6 (∀𝑢 ∈ ran (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)) → Fun ran )
208206, 207syl 17 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → Fun ran )
209132, 208syldan 591 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → Fun ran )
210 vex 3484 . . . . . . . . 9 𝑚 ∈ V
211210eldm2 5912 . . . . . . . 8 (𝑚 ∈ dom ran ↔ ∃𝑢𝑚, 𝑢⟩ ∈ ran )
212 eluni2 4911 . . . . . . . . . 10 (⟨𝑚, 𝑢⟩ ∈ ran ↔ ∃𝑣 ∈ ran 𝑚, 𝑢⟩ ∈ 𝑣)
213210, 141opeldm 5918 . . . . . . . . . . . . . . 15 (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ dom 𝑣)
214213a1i 11 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ dom 𝑣))
215133, 44sstrdi 3996 . . . . . . . . . . . . . . 15 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
216 ssel 3977 . . . . . . . . . . . . . . . 16 (ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
217 vex 3484 . . . . . . . . . . . . . . . . . 18 𝑣 ∈ V
218 dmeq 5914 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣)
219218eleq2d 2827 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣))
220218eleq1d 2826 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω))
221219, 220anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
222217, 221elab 3679 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))
223222simprbi 496 . . . . . . . . . . . . . . . 16 (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → dom 𝑣 ∈ ω)
224216, 223syl6 35 . . . . . . . . . . . . . . 15 (ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran → dom 𝑣 ∈ ω))
225215, 224syl 17 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (𝑣 ∈ ran → dom 𝑣 ∈ ω))
226214, 225anim12d 609 . . . . . . . . . . . . 13 (:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣𝑣 ∈ ran ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
227 elnn 7898 . . . . . . . . . . . . 13 ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω)
228226, 227syl6 35 . . . . . . . . . . . 12 (:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣𝑣 ∈ ran ) → 𝑚 ∈ ω))
229228expcomd 416 . . . . . . . . . . 11 (:ω⟶𝑆 → (𝑣 ∈ ran → (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ ω)))
230229rexlimdv 3153 . . . . . . . . . 10 (:ω⟶𝑆 → (∃𝑣 ∈ ran 𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ ω))
231212, 230biimtrid 242 . . . . . . . . 9 (:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ ran 𝑚 ∈ ω))
232231exlimdv 1933 . . . . . . . 8 (:ω⟶𝑆 → (∃𝑢𝑚, 𝑢⟩ ∈ ran 𝑚 ∈ ω))
233211, 232biimtrid 242 . . . . . . 7 (:ω⟶𝑆 → (𝑚 ∈ dom ran 𝑚 ∈ ω))
234233adantr 480 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom ran 𝑚 ∈ ω))
235 id 22 . . . . . . . . . . 11 (𝑚 ∈ ω → 𝑚 ∈ ω)
236 fnfvelrn 7100 . . . . . . . . . . 11 (( Fn ω ∧ 𝑚 ∈ ω) → (𝑚) ∈ ran )
237146, 235, 236syl2anr 597 . . . . . . . . . 10 ((𝑚 ∈ ω ∧ :ω⟶𝑆) → (𝑚) ∈ ran )
238237adantrr 717 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑚) ∈ ran )
239128simpld 494 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 ∈ dom (𝑚))
240 dmeq 5914 . . . . . . . . . 10 (𝑢 = (𝑚) → dom 𝑢 = dom (𝑚))
241240eliuni 4997 . . . . . . . . 9 (((𝑚) ∈ ran 𝑚 ∈ dom (𝑚)) → 𝑚 𝑢 ∈ ran dom 𝑢)
242238, 239, 241syl2anc 584 . . . . . . . 8 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 𝑢 ∈ ran dom 𝑢)
243 dmuni 5925 . . . . . . . 8 dom ran = 𝑢 ∈ ran dom 𝑢
244242, 243eleqtrrdi 2852 . . . . . . 7 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 ∈ dom ran )
245244expcom 413 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ran ))
246234, 245impbid 212 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom ran 𝑚 ∈ ω))
247246eqrdv 2735 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → dom ran = ω)
248 rnuni 6168 . . . . . 6 ran ran = 𝑠 ∈ ran ran 𝑠
249 frn 6743 . . . . . . . . . . . . . 14 (𝑠:suc 𝑛𝐴 → ran 𝑠𝐴)
2502493ad2ant1 1134 . . . . . . . . . . . . 13 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → ran 𝑠𝐴)
251250rexlimivw 3151 . . . . . . . . . . . 12 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → ran 𝑠𝐴)
252251ss2abi 4067 . . . . . . . . . . 11 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ ran 𝑠𝐴}
25328, 252eqsstri 4030 . . . . . . . . . 10 𝑆 ⊆ {𝑠 ∣ ran 𝑠𝐴}
254133, 253sstrdi 3996 . . . . . . . . 9 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ ran 𝑠𝐴})
255 ssel 3977 . . . . . . . . . 10 (ran ⊆ {𝑠 ∣ ran 𝑠𝐴} → (𝑠 ∈ ran 𝑠 ∈ {𝑠 ∣ ran 𝑠𝐴}))
256 abid 2718 . . . . . . . . . 10 (𝑠 ∈ {𝑠 ∣ ran 𝑠𝐴} ↔ ran 𝑠𝐴)
257255, 256imbitrdi 251 . . . . . . . . 9 (ran ⊆ {𝑠 ∣ ran 𝑠𝐴} → (𝑠 ∈ ran → ran 𝑠𝐴))
258254, 257syl 17 . . . . . . . 8 (:ω⟶𝑆 → (𝑠 ∈ ran → ran 𝑠𝐴))
259258ralrimiv 3145 . . . . . . 7 (:ω⟶𝑆 → ∀𝑠 ∈ ran ran 𝑠𝐴)
260 iunss 5045 . . . . . . 7 ( 𝑠 ∈ ran ran 𝑠𝐴 ↔ ∀𝑠 ∈ ran ran 𝑠𝐴)
261259, 260sylibr 234 . . . . . 6 (:ω⟶𝑆 𝑠 ∈ ran ran 𝑠𝐴)
262248, 261eqsstrid 4022 . . . . 5 (:ω⟶𝑆 → ran ran 𝐴)
263262adantr 480 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ran ran 𝐴)
264 df-fn 6564 . . . . 5 ( ran Fn ω ↔ (Fun ran ∧ dom ran = ω))
265 df-f 6565 . . . . . 6 ( ran :ω⟶𝐴 ↔ ( ran Fn ω ∧ ran ran 𝐴))
266265biimpri 228 . . . . 5 (( ran Fn ω ∧ ran ran 𝐴) → ran :ω⟶𝐴)
267264, 266sylanbr 582 . . . 4 (((Fun ran ∧ dom ran = ω) ∧ ran ran 𝐴) → ran :ω⟶𝐴)
268209, 247, 263, 267syl21anc 838 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ran :ω⟶𝐴)
269 fnfvelrn 7100 . . . . . . . 8 (( Fn ω ∧ ∅ ∈ ω) → (‘∅) ∈ ran )
270146, 25, 269sylancl 586 . . . . . . 7 (:ω⟶𝑆 → (‘∅) ∈ ran )
271270adantr 480 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘∅) ∈ ran )
272 elssuni 4937 . . . . . 6 ((‘∅) ∈ ran → (‘∅) ⊆ ran )
273271, 272syl 17 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘∅) ⊆ ran )
27454adantr 480 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∅ ∈ dom (‘∅))
275 funssfv 6927 . . . . 5 ((Fun ran ∧ (‘∅) ⊆ ran ∧ ∅ ∈ dom (‘∅)) → ( ran ‘∅) = ((‘∅)‘∅))
276209, 273, 274, 275syl3anc 1373 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ( ran ‘∅) = ((‘∅)‘∅))
277 simp2 1138 . . . . . . . . . . 11 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑠‘∅) = 𝐶)
278277rexlimivw 3151 . . . . . . . . . 10 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑠‘∅) = 𝐶)
279278ss2abi 4067 . . . . . . . . 9 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
28028, 279eqsstri 4030 . . . . . . . 8 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
281133, 280sstrdi 3996 . . . . . . 7 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶})
282 ssel 3977 . . . . . . . 8 (ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((‘∅) ∈ ran → (‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶}))
283 fveq1 6905 . . . . . . . . . 10 (𝑠 = (‘∅) → (𝑠‘∅) = ((‘∅)‘∅))
284283eqeq1d 2739 . . . . . . . . 9 (𝑠 = (‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((‘∅)‘∅) = 𝐶))
28546, 284elab 3679 . . . . . . . 8 ((‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((‘∅)‘∅) = 𝐶)
286282, 285imbitrdi 251 . . . . . . 7 (ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
287281, 286syl 17 . . . . . 6 (:ω⟶𝑆 → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
288287adantr 480 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
289271, 288mpd 15 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((‘∅)‘∅) = 𝐶)
290276, 289eqtrd 2777 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ( ran ‘∅) = 𝐶)
291 nfv 1914 . . . . 5 𝑘 :ω⟶𝑆
292 nfra1 3284 . . . . 5 𝑘𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))
293291, 292nfan 1899 . . . 4 𝑘(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))
294133ad2antrr 726 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ran 𝑆)
295 peano2 7912 . . . . . . . . 9 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
296 fnfvelrn 7100 . . . . . . . . 9 (( Fn ω ∧ suc 𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
297146, 295, 296syl2an 596 . . . . . . . 8 ((:ω⟶𝑆𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
298297adantlr 715 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
299239expcom 413 . . . . . . . . 9 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (𝑚)))
300299ralrimiv 3145 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚))
301 id 22 . . . . . . . . . . 11 (𝑚 = suc 𝑘𝑚 = suc 𝑘)
302 fveq2 6906 . . . . . . . . . . . 12 (𝑚 = suc 𝑘 → (𝑚) = (‘suc 𝑘))
303302dmeqd 5916 . . . . . . . . . . 11 (𝑚 = suc 𝑘 → dom (𝑚) = dom (‘suc 𝑘))
304301, 303eleq12d 2835 . . . . . . . . . 10 (𝑚 = suc 𝑘 → (𝑚 ∈ dom (𝑚) ↔ suc 𝑘 ∈ dom (‘suc 𝑘)))
305304rspcv 3618 . . . . . . . . 9 (suc 𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚) → suc 𝑘 ∈ dom (‘suc 𝑘)))
306295, 305syl 17 . . . . . . . 8 (𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚) → suc 𝑘 ∈ dom (‘suc 𝑘)))
307300, 306mpan9 506 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (‘suc 𝑘))
308 eleq2 2830 . . . . . . . . . . . . . . . . . . . . 21 (dom 𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛))
309308biimpa 476 . . . . . . . . . . . . . . . . . . . 20 ((dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
31029, 309sylan 580 . . . . . . . . . . . . . . . . . . 19 ((𝑠:suc 𝑛𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
311 ordsucelsuc 7842 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord 𝑛 → (𝑘𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
31230, 311syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ω → (𝑘𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
313312biimprd 248 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛𝑘𝑛))
314 rsp 3247 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑘𝑛 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))
315313, 314syl9r 78 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
316315com13 88 . . . . . . . . . . . . . . . . . . 19 (suc 𝑘 ∈ suc 𝑛 → (𝑛 ∈ ω → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
317310, 316syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑠:suc 𝑛𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → (𝑛 ∈ ω → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
318317ex 412 . . . . . . . . . . . . . . . . 17 (𝑠:suc 𝑛𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))))
319318com24 95 . . . . . . . . . . . . . . . 16 (𝑠:suc 𝑛𝐴 → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))))
320319imp 406 . . . . . . . . . . . . . . 15 ((𝑠:suc 𝑛𝐴 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
3213203adant2 1132 . . . . . . . . . . . . . 14 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
322321impcom 407 . . . . . . . . . . . . 13 ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))
323322rexlimiva 3147 . . . . . . . . . . . 12 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))
324323ss2abi 4067 . . . . . . . . . . 11 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
32528, 324eqsstri 4030 . . . . . . . . . 10 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
326 sstr 3992 . . . . . . . . . 10 ((ran 𝑆𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}) → ran ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))})
327325, 326mpan2 691 . . . . . . . . 9 (ran 𝑆 → ran ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))})
328327sseld 3982 . . . . . . . 8 (ran 𝑆 → ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}))
329 fvex 6919 . . . . . . . . 9 (‘suc 𝑘) ∈ V
330 dmeq 5914 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → dom 𝑠 = dom (‘suc 𝑘))
331330eleq2d 2827 . . . . . . . . . 10 (𝑠 = (‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (‘suc 𝑘)))
332 fveq1 6905 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → (𝑠‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
333 fveq1 6905 . . . . . . . . . . . 12 (𝑠 = (‘suc 𝑘) → (𝑠𝑘) = ((‘suc 𝑘)‘𝑘))
334333fveq2d 6910 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → (𝐹‘(𝑠𝑘)) = (𝐹‘((‘suc 𝑘)‘𝑘)))
335332, 334eleq12d 2835 . . . . . . . . . 10 (𝑠 = (‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) ↔ ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
336331, 335imbi12d 344 . . . . . . . . 9 (𝑠 = (‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) ↔ (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))))
337329, 336elab 3679 . . . . . . . 8 ((‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ↔ (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
338328, 337imbitrdi 251 . . . . . . 7 (ran 𝑆 → ((‘suc 𝑘) ∈ ran → (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))))
339294, 298, 307, 338syl3c 66 . . . . . 6 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))
340209adantr 480 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → Fun ran )
341 elssuni 4937 . . . . . . . . . 10 ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ⊆ ran )
342297, 341syl 17 . . . . . . . . 9 ((:ω⟶𝑆𝑘 ∈ ω) → (‘suc 𝑘) ⊆ ran )
343342adantlr 715 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ⊆ ran )
344 funssfv 6927 . . . . . . . 8 ((Fun ran ∧ (‘suc 𝑘) ⊆ ran ∧ suc 𝑘 ∈ dom (‘suc 𝑘)) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
345340, 343, 307, 344syl3anc 1373 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
346215sseld 3982 . . . . . . . . . . . . . . 15 (:ω⟶𝑆 → ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
347330eleq2d 2827 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (‘suc 𝑘)))
348330eleq1d 2826 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (‘suc 𝑘) ∈ ω))
349347, 348anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑠 = (‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
350329, 349elab 3679 . . . . . . . . . . . . . . 15 ((‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω))
351346, 350imbitrdi 251 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → ((‘suc 𝑘) ∈ ran → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
352351adantr 480 . . . . . . . . . . . . 13 ((:ω⟶𝑆𝑘 ∈ ω) → ((‘suc 𝑘) ∈ ran → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
353297, 352mpd 15 . . . . . . . . . . . 12 ((:ω⟶𝑆𝑘 ∈ ω) → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω))
354353simprd 495 . . . . . . . . . . 11 ((:ω⟶𝑆𝑘 ∈ ω) → dom (‘suc 𝑘) ∈ ω)
355 nnord 7895 . . . . . . . . . . 11 (dom (‘suc 𝑘) ∈ ω → Ord dom (‘suc 𝑘))
356 ordtr 6398 . . . . . . . . . . 11 (Ord dom (‘suc 𝑘) → Tr dom (‘suc 𝑘))
357 trsuc 6471 . . . . . . . . . . . 12 ((Tr dom (‘suc 𝑘) ∧ suc 𝑘 ∈ dom (‘suc 𝑘)) → 𝑘 ∈ dom (‘suc 𝑘))
358357ex 412 . . . . . . . . . . 11 (Tr dom (‘suc 𝑘) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
359354, 355, 356, 3584syl 19 . . . . . . . . . 10 ((:ω⟶𝑆𝑘 ∈ ω) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
360359adantlr 715 . . . . . . . . 9 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
361307, 360mpd 15 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom (‘suc 𝑘))
362 funssfv 6927 . . . . . . . 8 ((Fun ran ∧ (‘suc 𝑘) ⊆ ran 𝑘 ∈ dom (‘suc 𝑘)) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
363340, 343, 361, 362syl3anc 1373 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
364 simpl 482 . . . . . . . 8 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
365 simpr 484 . . . . . . . . 9 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
366365fveq2d 6910 . . . . . . . 8 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → (𝐹‘( ran 𝑘)) = (𝐹‘((‘suc 𝑘)‘𝑘)))
367364, 366eleq12d 2835 . . . . . . 7 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → (( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)) ↔ ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
368345, 363, 367syl2anc 584 . . . . . 6 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)) ↔ ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
369339, 368mpbird 257 . . . . 5 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))
370369ex 412 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑘 ∈ ω → ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
371293, 370ralrimi 3257 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))
372 vex 3484 . . . . . 6 ∈ V
373372rnex 7932 . . . . 5 ran ∈ V
374373uniex 7761 . . . 4 ran ∈ V
375 feq1 6716 . . . . 5 (𝑔 = ran → (𝑔:ω⟶𝐴 ran :ω⟶𝐴))
376 fveq1 6905 . . . . . 6 (𝑔 = ran → (𝑔‘∅) = ( ran ‘∅))
377376eqeq1d 2739 . . . . 5 (𝑔 = ran → ((𝑔‘∅) = 𝐶 ↔ ( ran ‘∅) = 𝐶))
378 fveq1 6905 . . . . . . 7 (𝑔 = ran → (𝑔‘suc 𝑘) = ( ran ‘suc 𝑘))
379 fveq1 6905 . . . . . . . 8 (𝑔 = ran → (𝑔𝑘) = ( ran 𝑘))
380379fveq2d 6910 . . . . . . 7 (𝑔 = ran → (𝐹‘(𝑔𝑘)) = (𝐹‘( ran 𝑘)))
381378, 380eleq12d 2835 . . . . . 6 (𝑔 = ran → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
382381ralbidv 3178 . . . . 5 (𝑔 = ran → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
383375, 377, 3823anbi123d 1438 . . . 4 (𝑔 = ran → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))) ↔ ( ran :ω⟶𝐴 ∧ ( ran ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))))
384374, 383spcev 3606 . . 3 (( ran :ω⟶𝐴 ∧ ( ran ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
385268, 290, 371, 384syl3anc 1373 . 2 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
386385exlimiv 1930 1 (∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848  w3o 1086  w3a 1087   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  wss 3951  c0 4333  cop 4632   cuni 4907   ciun 4991  cmpt 5225  Tr wtr 5259  dom cdm 5685  ran crn 5686  cres 5687  Ord word 6383  suc csuc 6386  Fun wfun 6555   Fn wfn 6556  wf 6557  cfv 6561  ωcom 7887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-dc 10486
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-om 7888  df-1o 8506
This theorem is referenced by:  axdc3lem4  10493
  Copyright terms: Public domain W3C validator