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

Theorem axdc3lem2 10446
Description: Lemma for axdc3 10449. 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 10441 (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 10441 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 6892 . . . . . . . . . . . . . 14 (𝑚 = ∅ → (𝑚) = (‘∅))
32dmeqd 5906 . . . . . . . . . . . . 13 (𝑚 = ∅ → dom (𝑚) = dom (‘∅))
41, 3eleq12d 2828 . . . . . . . . . . . 12 (𝑚 = ∅ → (𝑚 ∈ dom (𝑚) ↔ ∅ ∈ dom (‘∅)))
5 eleq2 2823 . . . . . . . . . . . . 13 (𝑚 = ∅ → (𝑗𝑚𝑗 ∈ ∅))
62sseq2d 4015 . . . . . . . . . . . . 13 (𝑚 = ∅ → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (‘∅)))
75, 6imbi12d 345 . . . . . . . . . . . 12 (𝑚 = ∅ → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
84, 7anbi12d 632 . . . . . . . . . . 11 (𝑚 = ∅ → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅)))))
9 id 22 . . . . . . . . . . . . 13 (𝑚 = 𝑖𝑚 = 𝑖)
10 fveq2 6892 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → (𝑚) = (𝑖))
1110dmeqd 5906 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → dom (𝑚) = dom (𝑖))
129, 11eleq12d 2828 . . . . . . . . . . . 12 (𝑚 = 𝑖 → (𝑚 ∈ dom (𝑚) ↔ 𝑖 ∈ dom (𝑖)))
13 elequ2 2122 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → (𝑗𝑚𝑗𝑖))
1410sseq2d 4015 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑖)))
1513, 14imbi12d 345 . . . . . . . . . . . 12 (𝑚 = 𝑖 → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗𝑖 → (𝑗) ⊆ (𝑖))))
1612, 15anbi12d 632 . . . . . . . . . . 11 (𝑚 = 𝑖 → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖)))))
17 id 22 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖𝑚 = suc 𝑖)
18 fveq2 6892 . . . . . . . . . . . . . 14 (𝑚 = suc 𝑖 → (𝑚) = (‘suc 𝑖))
1918dmeqd 5906 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → dom (𝑚) = dom (‘suc 𝑖))
2017, 19eleq12d 2828 . . . . . . . . . . . 12 (𝑚 = suc 𝑖 → (𝑚 ∈ dom (𝑚) ↔ suc 𝑖 ∈ dom (‘suc 𝑖)))
21 eleq2 2823 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → (𝑗𝑚𝑗 ∈ suc 𝑖))
2218sseq2d 4015 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (‘suc 𝑖)))
2321, 22imbi12d 345 . . . . . . . . . . . 12 (𝑚 = suc 𝑖 → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))
2420, 23anbi12d 632 . . . . . . . . . . 11 (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
25 peano1 7879 . . . . . . . . . . . . . . 15 ∅ ∈ ω
26 ffvelcdm 7084 . . . . . . . . . . . . . . 15 ((:ω⟶𝑆 ∧ ∅ ∈ ω) → (‘∅) ∈ 𝑆)
2725, 26mpan2 690 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (‘∅) ∈ 𝑆)
28 axdc3lem2.2 . . . . . . . . . . . . . . . . . 18 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
29 fdm 6727 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠:suc 𝑛𝐴 → dom 𝑠 = suc 𝑛)
30 nnord 7863 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ω → Ord 𝑛)
31 0elsuc 7823 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝑛 → ∅ ∈ suc 𝑛)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → ∅ ∈ suc 𝑛)
33 peano2 7881 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
34 eleq2 2823 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛))
35 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω))
3634, 35anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom 𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω)))
3736biimprcd 249 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
3832, 33, 37syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ω → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
3929, 38syl5com 31 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠:suc 𝑛𝐴 → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
40393ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
4140impcom 409 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
4241rexlimiva 3148 . . . . . . . . . . . . . . . . . . 19 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
4342ss2abi 4064 . . . . . . . . . . . . . . . . . 18 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
4428, 43eqsstri 4017 . . . . . . . . . . . . . . . . 17 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
4544sseli 3979 . . . . . . . . . . . . . . . 16 ((‘∅) ∈ 𝑆 → (‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
46 fvex 6905 . . . . . . . . . . . . . . . . 17 (‘∅) ∈ V
47 dmeq 5904 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (‘∅) → dom 𝑠 = dom (‘∅))
4847eleq2d 2820 . . . . . . . . . . . . . . . . . 18 (𝑠 = (‘∅) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (‘∅)))
4947eleq1d 2819 . . . . . . . . . . . . . . . . . 18 (𝑠 = (‘∅) → (dom 𝑠 ∈ ω ↔ dom (‘∅) ∈ ω))
5048, 49anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘∅) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω)))
5146, 50elab 3669 . . . . . . . . . . . . . . . 16 ((‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω))
5245, 51sylib 217 . . . . . . . . . . . . . . 15 ((‘∅) ∈ 𝑆 → (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω))
5352simpld 496 . . . . . . . . . . . . . 14 ((‘∅) ∈ 𝑆 → ∅ ∈ dom (‘∅))
5427, 53syl 17 . . . . . . . . . . . . 13 (:ω⟶𝑆 → ∅ ∈ dom (‘∅))
55 noel 4331 . . . . . . . . . . . . . 14 ¬ 𝑗 ∈ ∅
5655pm2.21i 119 . . . . . . . . . . . . 13 (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))
5754, 56jctir 522 . . . . . . . . . . . 12 (:ω⟶𝑆 → (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
5857adantr 482 . . . . . . . . . . 11 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
59 ffvelcdm 7084 . . . . . . . . . . . . . . 15 ((:ω⟶𝑆𝑖 ∈ ω) → (𝑖) ∈ 𝑆)
6059ancoms 460 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ :ω⟶𝑆) → (𝑖) ∈ 𝑆)
6160adantrr 716 . . . . . . . . . . . . 13 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑖) ∈ 𝑆)
62 suceq 6431 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
6362fveq2d 6896 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (‘suc 𝑘) = (‘suc 𝑖))
64 2fveq3 6897 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (𝐺‘(𝑘)) = (𝐺‘(𝑖)))
6563, 64eleq12d 2828 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((‘suc 𝑘) ∈ (𝐺‘(𝑘)) ↔ (‘suc 𝑖) ∈ (𝐺‘(𝑖))))
6665rspcva 3611 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘suc 𝑖) ∈ (𝐺‘(𝑖)))
6766adantrl 715 . . . . . . . . . . . . 13 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (‘suc 𝑖) ∈ (𝐺‘(𝑖)))
6844sseli 3979 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ 𝑆 → (𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
69 fvex 6905 . . . . . . . . . . . . . . . . . . . . 21 (𝑖) ∈ V
70 dmeq 5904 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑖) → dom 𝑠 = dom (𝑖))
7170eleq2d 2820 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (𝑖)))
7270eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑖) → (dom 𝑠 ∈ ω ↔ dom (𝑖) ∈ ω))
7371, 72anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω)))
7469, 73elab 3669 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω))
7568, 74sylib 217 . . . . . . . . . . . . . . . . . . 19 ((𝑖) ∈ 𝑆 → (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω))
7675simprd 497 . . . . . . . . . . . . . . . . . 18 ((𝑖) ∈ 𝑆 → dom (𝑖) ∈ ω)
77 nnord 7863 . . . . . . . . . . . . . . . . . 18 (dom (𝑖) ∈ ω → Ord dom (𝑖))
78 ordsucelsuc 7810 . . . . . . . . . . . . . . . . . 18 (Ord dom (𝑖) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
7976, 77, 783syl 18 . . . . . . . . . . . . . . . . 17 ((𝑖) ∈ 𝑆 → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
8079adantr 482 . . . . . . . . . . . . . . . 16 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
81 dmeq 5904 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑖) → dom 𝑥 = dom (𝑖))
82 suceq 6431 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑥 = dom (𝑖) → suc dom 𝑥 = suc dom (𝑖))
8381, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → suc dom 𝑥 = suc dom (𝑖))
8483eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (𝑖)))
8581reseq2d 5982 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (𝑖)))
86 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → 𝑥 = (𝑖))
8785, 86eqeq12d 2749 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (𝑖)) = (𝑖)))
8884, 87anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑖) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))))
8988rabbidv 3441 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑖) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))})
90 axdc3lem2.3 . . . . . . . . . . . . . . . . . . . . . 22 𝐺 = (𝑥𝑆 ↦ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
91 axdc3lem2.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝐴 ∈ V
9291, 28axdc3lem 10445 . . . . . . . . . . . . . . . . . . . . . . 23 𝑆 ∈ V
9392rabex 5333 . . . . . . . . . . . . . . . . . . . . . 22 {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))} ∈ V
9489, 90, 93fvmpt 6999 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖) ∈ 𝑆 → (𝐺‘(𝑖)) = {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))})
9594eleq2d 2820 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ 𝑆 → ((‘suc 𝑖) ∈ (𝐺‘(𝑖)) ↔ (‘suc 𝑖) ∈ {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))}))
96 dmeq 5904 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (‘suc 𝑖) → dom 𝑦 = dom (‘suc 𝑖))
9796eqeq1d 2735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (‘suc 𝑖) → (dom 𝑦 = suc dom (𝑖) ↔ dom (‘suc 𝑖) = suc dom (𝑖)))
98 reseq1 5976 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (‘suc 𝑖) → (𝑦 ↾ dom (𝑖)) = ((‘suc 𝑖) ↾ dom (𝑖)))
9998eqeq1d 2735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (‘suc 𝑖) → ((𝑦 ↾ dom (𝑖)) = (𝑖) ↔ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))
10097, 99anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (‘suc 𝑖) → ((dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖)) ↔ (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖))))
101100elrab 3684 . . . . . . . . . . . . . . . . . . . 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 501 . . . . . . . . . . . . . . . . . 18 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))
104103simpld 496 . . . . . . . . . . . . . . . . 17 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → dom (‘suc 𝑖) = suc dom (𝑖))
105104eleq2d 2820 . . . . . . . . . . . . . . . 16 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
10680, 105bitr4d 282 . . . . . . . . . . . . . . 15 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ dom (‘suc 𝑖)))
107106biimpd 228 . . . . . . . . . . . . . 14 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) → suc 𝑖 ∈ dom (‘suc 𝑖)))
108103simprd 497 . . . . . . . . . . . . . . 15 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖))
109 resss 6007 . . . . . . . . . . . . . . . 16 ((‘suc 𝑖) ↾ dom (𝑖)) ⊆ (‘suc 𝑖)
110 sseq1 4008 . . . . . . . . . . . . . . . 16 (((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖) → (((‘suc 𝑖) ↾ dom (𝑖)) ⊆ (‘suc 𝑖) ↔ (𝑖) ⊆ (‘suc 𝑖)))
111109, 110mpbii 232 . . . . . . . . . . . . . . 15 (((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖) → (𝑖) ⊆ (‘suc 𝑖))
112 elsuci 6432 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ suc 𝑖 → (𝑗𝑖𝑗 = 𝑖))
113 pm2.27 42 . . . . . . . . . . . . . . . . . . 19 (𝑗𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → (𝑗) ⊆ (𝑖)))
114 sstr2 3990 . . . . . . . . . . . . . . . . . . 19 ((𝑗) ⊆ (𝑖) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖)))
115113, 114syl6 35 . . . . . . . . . . . . . . . . . 18 (𝑗𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
116 fveq2 6892 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝑗) = (𝑖))
117116sseq1d 4014 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → ((𝑗) ⊆ (‘suc 𝑖) ↔ (𝑖) ⊆ (‘suc 𝑖)))
118117biimprd 247 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖)))
119118a1d 25 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
120115, 119jaoi 856 . . . . . . . . . . . . . . . . 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 610 . . . . . . . . . . . . 13 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
12561, 67, 124syl2anc 585 . . . . . . . . . . . 12 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
126125ex 414 . . . . . . . . . . 11 (𝑖 ∈ ω → ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))))
1278, 16, 24, 58, 126finds2 7891 . . . . . . . . . 10 (𝑚 ∈ ω → ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚)))))
128127imp 408 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))))
129128simprd 497 . . . . . . . 8 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑗𝑚 → (𝑗) ⊆ (𝑚)))
130129expcom 415 . . . . . . 7 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → (𝑗𝑚 → (𝑗) ⊆ (𝑚))))
131130ralrimdv 3153 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → ∀𝑗𝑚 (𝑗) ⊆ (𝑚)))
132131ralrimiv 3146 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚))
133 frn 6725 . . . . . . . . . . . 12 (:ω⟶𝑆 → ran 𝑆)
134 ffun 6721 . . . . . . . . . . . . . . . 16 (𝑠:suc 𝑛𝐴 → Fun 𝑠)
1351343ad2ant1 1134 . . . . . . . . . . . . . . 15 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → Fun 𝑠)
136135rexlimivw 3152 . . . . . . . . . . . . . 14 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → Fun 𝑠)
137136ss2abi 4064 . . . . . . . . . . . . 13 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠}
13828, 137eqsstri 4017 . . . . . . . . . . . 12 𝑆 ⊆ {𝑠 ∣ Fun 𝑠}
139133, 138sstrdi 3995 . . . . . . . . . . 11 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ Fun 𝑠})
140139sseld 3982 . . . . . . . . . 10 (:ω⟶𝑆 → (𝑢 ∈ ran 𝑢 ∈ {𝑠 ∣ Fun 𝑠}))
141 vex 3479 . . . . . . . . . . 11 𝑢 ∈ V
142 funeq 6569 . . . . . . . . . . 11 (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢))
143141, 142elab 3669 . . . . . . . . . 10 (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢)
144140, 143imbitrdi 250 . . . . . . . . 9 (:ω⟶𝑆 → (𝑢 ∈ ran → Fun 𝑢))
145144adantr 482 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → Fun 𝑢))
146 ffn 6718 . . . . . . . . 9 (:ω⟶𝑆 Fn ω)
147 fvelrnb 6953 . . . . . . . . . . . . 13 ( Fn ω → (𝑣 ∈ ran ↔ ∃𝑏 ∈ ω (𝑏) = 𝑣))
148 fvelrnb 6953 . . . . . . . . . . . . . . 15 ( Fn ω → (𝑢 ∈ ran ↔ ∃𝑎 ∈ ω (𝑎) = 𝑢))
149 nnord 7863 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ω → Ord 𝑎)
150 nnord 7863 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ ω → Ord 𝑏)
151149, 150anim12i 614 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord 𝑎 ∧ Ord 𝑏))
152 ordtri3or 6397 . . . . . . . . . . . . . . . . . . . . . . 23 ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎𝑏𝑎 = 𝑏𝑏𝑎))
153 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑏 → (𝑚) = (𝑏))
154153sseq2d 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑏 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑏)))
155154raleqbi1dv 3334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 = 𝑏 → (∀𝑗𝑚 (𝑗) ⊆ (𝑚) ↔ ∀𝑗𝑏 (𝑗) ⊆ (𝑏)))
156155rspcv 3609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ∀𝑗𝑏 (𝑗) ⊆ (𝑏)))
157 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑎 → (𝑗) = (𝑎))
158157sseq1d 4014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑎 → ((𝑗) ⊆ (𝑏) ↔ (𝑎) ⊆ (𝑏)))
159158rspccv 3610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑗𝑏 (𝑗) ⊆ (𝑏) → (𝑎𝑏 → (𝑎) ⊆ (𝑏)))
160156, 159syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → (𝑎) ⊆ (𝑏))))
161160adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → (𝑎) ⊆ (𝑏))))
1621613imp 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑎𝑏) → (𝑎) ⊆ (𝑏))
163162orcd 872 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑎𝑏) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1641633exp 1120 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
165164com3r 87 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
166 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑏 → (𝑎) = (𝑏))
167 eqimss 4041 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎) = (𝑏) → (𝑎) ⊆ (𝑏))
168167orcd 872 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎) = (𝑏) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
169166, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑏 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1701692a1d 26 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
171 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑎 → (𝑚) = (𝑎))
172171sseq2d 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑎 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑎)))
173172raleqbi1dv 3334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 = 𝑎 → (∀𝑗𝑚 (𝑗) ⊆ (𝑚) ↔ ∀𝑗𝑎 (𝑗) ⊆ (𝑎)))
174173rspcv 3609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ∀𝑗𝑎 (𝑗) ⊆ (𝑎)))
175 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑏 → (𝑗) = (𝑏))
176175sseq1d 4014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑏 → ((𝑗) ⊆ (𝑎) ↔ (𝑏) ⊆ (𝑎)))
177176rspccv 3610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑗𝑎 (𝑗) ⊆ (𝑎) → (𝑏𝑎 → (𝑏) ⊆ (𝑎)))
178174, 177syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → (𝑏) ⊆ (𝑎))))
179178adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → (𝑏) ⊆ (𝑎))))
1801793imp 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑏𝑎) → (𝑏) ⊆ (𝑎))
181180olcd 873 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑏𝑎) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1821813exp 1120 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
183182com3r 87 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
184165, 170, 1833jaoi 1428 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑏𝑎 = 𝑏𝑏𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
185152, 184syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord 𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
186151, 185mpcom 38 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎))))
187 sseq12 4010 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → ((𝑎) ⊆ (𝑏) ↔ 𝑢𝑣))
188 sseq12 4010 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑏) = 𝑣 ∧ (𝑎) = 𝑢) → ((𝑏) ⊆ (𝑎) ↔ 𝑣𝑢))
189188ancoms 460 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → ((𝑏) ⊆ (𝑎) ↔ 𝑣𝑢))
190187, 189orbi12d 918 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)) ↔ (𝑢𝑣𝑣𝑢)))
191190biimpcd 248 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (𝑢𝑣𝑣𝑢)))
192186, 191syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (𝑢𝑣𝑣𝑢))))
193192com23 86 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))
194193exp4b 432 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ω → (𝑏 ∈ ω → ((𝑎) = 𝑢 → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))))
195194com23 86 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ω → ((𝑎) = 𝑢 → (𝑏 ∈ ω → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))))
196195rexlimiv 3149 . . . . . . . . . . . . . . . 16 (∃𝑎 ∈ ω (𝑎) = 𝑢 → (𝑏 ∈ ω → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
197196rexlimdv 3154 . . . . . . . . . . . . . . 15 (∃𝑎 ∈ ω (𝑎) = 𝑢 → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))
198148, 197syl6bi 253 . . . . . . . . . . . . . 14 ( Fn ω → (𝑢 ∈ ran → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
199198com23 86 . . . . . . . . . . . . 13 ( Fn ω → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (𝑢 ∈ ran → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
200147, 199sylbid 239 . . . . . . . . . . . 12 ( Fn ω → (𝑣 ∈ ran → (𝑢 ∈ ran → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
201200com24 95 . . . . . . . . . . 11 ( Fn ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢 ∈ ran → (𝑣 ∈ ran → (𝑢𝑣𝑣𝑢)))))
202201imp 408 . . . . . . . . . 10 (( Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → (𝑣 ∈ ran → (𝑢𝑣𝑣𝑢))))
203202ralrimdv 3153 . . . . . . . . 9 (( Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
204146, 203sylan 581 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
205145, 204jcad 514 . . . . . . 7 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢))))
206205ralrimiv 3146 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → ∀𝑢 ∈ ran (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
207 fununi 6624 . . . . . 6 (∀𝑢 ∈ ran (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)) → Fun ran )
208206, 207syl 17 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → Fun ran )
209132, 208syldan 592 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → Fun ran )
210 vex 3479 . . . . . . . . 9 𝑚 ∈ V
211210eldm2 5902 . . . . . . . 8 (𝑚 ∈ dom ran ↔ ∃𝑢𝑚, 𝑢⟩ ∈ ran )
212 eluni2 4913 . . . . . . . . . 10 (⟨𝑚, 𝑢⟩ ∈ ran ↔ ∃𝑣 ∈ ran 𝑚, 𝑢⟩ ∈ 𝑣)
213210, 141opeldm 5908 . . . . . . . . . . . . . . 15 (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ dom 𝑣)
214213a1i 11 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ dom 𝑣))
215133, 44sstrdi 3995 . . . . . . . . . . . . . . 15 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
216 ssel 3976 . . . . . . . . . . . . . . . 16 (ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
217 vex 3479 . . . . . . . . . . . . . . . . . 18 𝑣 ∈ V
218 dmeq 5904 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣)
219218eleq2d 2820 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣))
220218eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω))
221219, 220anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
222217, 221elab 3669 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))
223222simprbi 498 . . . . . . . . . . . . . . . 16 (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → dom 𝑣 ∈ ω)
224216, 223syl6 35 . . . . . . . . . . . . . . 15 (ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran → dom 𝑣 ∈ ω))
225215, 224syl 17 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (𝑣 ∈ ran → dom 𝑣 ∈ ω))
226214, 225anim12d 610 . . . . . . . . . . . . 13 (:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣𝑣 ∈ ran ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
227 elnn 7866 . . . . . . . . . . . . 13 ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω)
228226, 227syl6 35 . . . . . . . . . . . 12 (:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣𝑣 ∈ ran ) → 𝑚 ∈ ω))
229228expcomd 418 . . . . . . . . . . 11 (:ω⟶𝑆 → (𝑣 ∈ ran → (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ ω)))
230229rexlimdv 3154 . . . . . . . . . 10 (:ω⟶𝑆 → (∃𝑣 ∈ ran 𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ ω))
231212, 230biimtrid 241 . . . . . . . . 9 (:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ ran 𝑚 ∈ ω))
232231exlimdv 1937 . . . . . . . 8 (:ω⟶𝑆 → (∃𝑢𝑚, 𝑢⟩ ∈ ran 𝑚 ∈ ω))
233211, 232biimtrid 241 . . . . . . 7 (:ω⟶𝑆 → (𝑚 ∈ dom ran 𝑚 ∈ ω))
234233adantr 482 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom ran 𝑚 ∈ ω))
235 id 22 . . . . . . . . . . 11 (𝑚 ∈ ω → 𝑚 ∈ ω)
236 fnfvelrn 7083 . . . . . . . . . . 11 (( Fn ω ∧ 𝑚 ∈ ω) → (𝑚) ∈ ran )
237146, 235, 236syl2anr 598 . . . . . . . . . 10 ((𝑚 ∈ ω ∧ :ω⟶𝑆) → (𝑚) ∈ ran )
238237adantrr 716 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑚) ∈ ran )
239128simpld 496 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 ∈ dom (𝑚))
240 dmeq 5904 . . . . . . . . . 10 (𝑢 = (𝑚) → dom 𝑢 = dom (𝑚))
241240eliuni 5004 . . . . . . . . 9 (((𝑚) ∈ ran 𝑚 ∈ dom (𝑚)) → 𝑚 𝑢 ∈ ran dom 𝑢)
242238, 239, 241syl2anc 585 . . . . . . . 8 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 𝑢 ∈ ran dom 𝑢)
243 dmuni 5915 . . . . . . . 8 dom ran = 𝑢 ∈ ran dom 𝑢
244242, 243eleqtrrdi 2845 . . . . . . 7 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 ∈ dom ran )
245244expcom 415 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ran ))
246234, 245impbid 211 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom ran 𝑚 ∈ ω))
247246eqrdv 2731 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → dom ran = ω)
248 rnuni 6149 . . . . . 6 ran ran = 𝑠 ∈ ran ran 𝑠
249 frn 6725 . . . . . . . . . . . . . 14 (𝑠:suc 𝑛𝐴 → ran 𝑠𝐴)
2502493ad2ant1 1134 . . . . . . . . . . . . 13 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → ran 𝑠𝐴)
251250rexlimivw 3152 . . . . . . . . . . . 12 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → ran 𝑠𝐴)
252251ss2abi 4064 . . . . . . . . . . 11 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ ran 𝑠𝐴}
25328, 252eqsstri 4017 . . . . . . . . . 10 𝑆 ⊆ {𝑠 ∣ ran 𝑠𝐴}
254133, 253sstrdi 3995 . . . . . . . . 9 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ ran 𝑠𝐴})
255 ssel 3976 . . . . . . . . . 10 (ran ⊆ {𝑠 ∣ ran 𝑠𝐴} → (𝑠 ∈ ran 𝑠 ∈ {𝑠 ∣ ran 𝑠𝐴}))
256 abid 2714 . . . . . . . . . 10 (𝑠 ∈ {𝑠 ∣ ran 𝑠𝐴} ↔ ran 𝑠𝐴)
257255, 256imbitrdi 250 . . . . . . . . 9 (ran ⊆ {𝑠 ∣ ran 𝑠𝐴} → (𝑠 ∈ ran → ran 𝑠𝐴))
258254, 257syl 17 . . . . . . . 8 (:ω⟶𝑆 → (𝑠 ∈ ran → ran 𝑠𝐴))
259258ralrimiv 3146 . . . . . . 7 (:ω⟶𝑆 → ∀𝑠 ∈ ran ran 𝑠𝐴)
260 iunss 5049 . . . . . . 7 ( 𝑠 ∈ ran ran 𝑠𝐴 ↔ ∀𝑠 ∈ ran ran 𝑠𝐴)
261259, 260sylibr 233 . . . . . 6 (:ω⟶𝑆 𝑠 ∈ ran ran 𝑠𝐴)
262248, 261eqsstrid 4031 . . . . 5 (:ω⟶𝑆 → ran ran 𝐴)
263262adantr 482 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ran ran 𝐴)
264 df-fn 6547 . . . . 5 ( ran Fn ω ↔ (Fun ran ∧ dom ran = ω))
265 df-f 6548 . . . . . 6 ( ran :ω⟶𝐴 ↔ ( ran Fn ω ∧ ran ran 𝐴))
266265biimpri 227 . . . . 5 (( ran Fn ω ∧ ran ran 𝐴) → ran :ω⟶𝐴)
267264, 266sylanbr 583 . . . 4 (((Fun ran ∧ dom ran = ω) ∧ ran ran 𝐴) → ran :ω⟶𝐴)
268209, 247, 263, 267syl21anc 837 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ran :ω⟶𝐴)
269 fnfvelrn 7083 . . . . . . . 8 (( Fn ω ∧ ∅ ∈ ω) → (‘∅) ∈ ran )
270146, 25, 269sylancl 587 . . . . . . 7 (:ω⟶𝑆 → (‘∅) ∈ ran )
271270adantr 482 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘∅) ∈ ran )
272 elssuni 4942 . . . . . 6 ((‘∅) ∈ ran → (‘∅) ⊆ ran )
273271, 272syl 17 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘∅) ⊆ ran )
27454adantr 482 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∅ ∈ dom (‘∅))
275 funssfv 6913 . . . . 5 ((Fun ran ∧ (‘∅) ⊆ ran ∧ ∅ ∈ dom (‘∅)) → ( ran ‘∅) = ((‘∅)‘∅))
276209, 273, 274, 275syl3anc 1372 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ( ran ‘∅) = ((‘∅)‘∅))
277 simp2 1138 . . . . . . . . . . 11 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑠‘∅) = 𝐶)
278277rexlimivw 3152 . . . . . . . . . 10 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑠‘∅) = 𝐶)
279278ss2abi 4064 . . . . . . . . 9 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
28028, 279eqsstri 4017 . . . . . . . 8 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
281133, 280sstrdi 3995 . . . . . . 7 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶})
282 ssel 3976 . . . . . . . 8 (ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((‘∅) ∈ ran → (‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶}))
283 fveq1 6891 . . . . . . . . . 10 (𝑠 = (‘∅) → (𝑠‘∅) = ((‘∅)‘∅))
284283eqeq1d 2735 . . . . . . . . 9 (𝑠 = (‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((‘∅)‘∅) = 𝐶))
28546, 284elab 3669 . . . . . . . 8 ((‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((‘∅)‘∅) = 𝐶)
286282, 285imbitrdi 250 . . . . . . 7 (ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
287281, 286syl 17 . . . . . 6 (:ω⟶𝑆 → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
288287adantr 482 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
289271, 288mpd 15 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((‘∅)‘∅) = 𝐶)
290276, 289eqtrd 2773 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ( ran ‘∅) = 𝐶)
291 nfv 1918 . . . . 5 𝑘 :ω⟶𝑆
292 nfra1 3282 . . . . 5 𝑘𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))
293291, 292nfan 1903 . . . 4 𝑘(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))
294133ad2antrr 725 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ran 𝑆)
295 peano2 7881 . . . . . . . . 9 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
296 fnfvelrn 7083 . . . . . . . . 9 (( Fn ω ∧ suc 𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
297146, 295, 296syl2an 597 . . . . . . . 8 ((:ω⟶𝑆𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
298297adantlr 714 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
299239expcom 415 . . . . . . . . 9 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (𝑚)))
300299ralrimiv 3146 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚))
301 id 22 . . . . . . . . . . 11 (𝑚 = suc 𝑘𝑚 = suc 𝑘)
302 fveq2 6892 . . . . . . . . . . . 12 (𝑚 = suc 𝑘 → (𝑚) = (‘suc 𝑘))
303302dmeqd 5906 . . . . . . . . . . 11 (𝑚 = suc 𝑘 → dom (𝑚) = dom (‘suc 𝑘))
304301, 303eleq12d 2828 . . . . . . . . . 10 (𝑚 = suc 𝑘 → (𝑚 ∈ dom (𝑚) ↔ suc 𝑘 ∈ dom (‘suc 𝑘)))
305304rspcv 3609 . . . . . . . . 9 (suc 𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚) → suc 𝑘 ∈ dom (‘suc 𝑘)))
306295, 305syl 17 . . . . . . . 8 (𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚) → suc 𝑘 ∈ dom (‘suc 𝑘)))
307300, 306mpan9 508 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (‘suc 𝑘))
308 eleq2 2823 . . . . . . . . . . . . . . . . . . . . 21 (dom 𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛))
309308biimpa 478 . . . . . . . . . . . . . . . . . . . 20 ((dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
31029, 309sylan 581 . . . . . . . . . . . . . . . . . . 19 ((𝑠:suc 𝑛𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
311 ordsucelsuc 7810 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord 𝑛 → (𝑘𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
31230, 311syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ω → (𝑘𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
313312biimprd 247 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛𝑘𝑛))
314 rsp 3245 . . . . . . . . . . . . . . . . . . . . 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 414 . . . . . . . . . . . . . . . . 17 (𝑠:suc 𝑛𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))))
319318com24 95 . . . . . . . . . . . . . . . 16 (𝑠:suc 𝑛𝐴 → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))))
320319imp 408 . . . . . . . . . . . . . . 15 ((𝑠:suc 𝑛𝐴 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
3213203adant2 1132 . . . . . . . . . . . . . 14 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
322321impcom 409 . . . . . . . . . . . . 13 ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))
323322rexlimiva 3148 . . . . . . . . . . . 12 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))
324323ss2abi 4064 . . . . . . . . . . 11 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
32528, 324eqsstri 4017 . . . . . . . . . 10 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
326 sstr 3991 . . . . . . . . . 10 ((ran 𝑆𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}) → ran ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))})
327325, 326mpan2 690 . . . . . . . . 9 (ran 𝑆 → ran ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))})
328327sseld 3982 . . . . . . . 8 (ran 𝑆 → ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}))
329 fvex 6905 . . . . . . . . 9 (‘suc 𝑘) ∈ V
330 dmeq 5904 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → dom 𝑠 = dom (‘suc 𝑘))
331330eleq2d 2820 . . . . . . . . . 10 (𝑠 = (‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (‘suc 𝑘)))
332 fveq1 6891 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → (𝑠‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
333 fveq1 6891 . . . . . . . . . . . 12 (𝑠 = (‘suc 𝑘) → (𝑠𝑘) = ((‘suc 𝑘)‘𝑘))
334333fveq2d 6896 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → (𝐹‘(𝑠𝑘)) = (𝐹‘((‘suc 𝑘)‘𝑘)))
335332, 334eleq12d 2828 . . . . . . . . . 10 (𝑠 = (‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) ↔ ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
336331, 335imbi12d 345 . . . . . . . . 9 (𝑠 = (‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) ↔ (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))))
337329, 336elab 3669 . . . . . . . 8 ((‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ↔ (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
338328, 337imbitrdi 250 . . . . . . 7 (ran 𝑆 → ((‘suc 𝑘) ∈ ran → (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))))
339294, 298, 307, 338syl3c 66 . . . . . 6 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))
340209adantr 482 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → Fun ran )
341 elssuni 4942 . . . . . . . . . 10 ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ⊆ ran )
342297, 341syl 17 . . . . . . . . 9 ((:ω⟶𝑆𝑘 ∈ ω) → (‘suc 𝑘) ⊆ ran )
343342adantlr 714 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ⊆ ran )
344 funssfv 6913 . . . . . . . 8 ((Fun ran ∧ (‘suc 𝑘) ⊆ ran ∧ suc 𝑘 ∈ dom (‘suc 𝑘)) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
345340, 343, 307, 344syl3anc 1372 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
346215sseld 3982 . . . . . . . . . . . . . . 15 (:ω⟶𝑆 → ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
347330eleq2d 2820 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (‘suc 𝑘)))
348330eleq1d 2819 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (‘suc 𝑘) ∈ ω))
349347, 348anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑠 = (‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
350329, 349elab 3669 . . . . . . . . . . . . . . 15 ((‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω))
351346, 350imbitrdi 250 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → ((‘suc 𝑘) ∈ ran → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
352351adantr 482 . . . . . . . . . . . . 13 ((:ω⟶𝑆𝑘 ∈ ω) → ((‘suc 𝑘) ∈ ran → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
353297, 352mpd 15 . . . . . . . . . . . 12 ((:ω⟶𝑆𝑘 ∈ ω) → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω))
354353simprd 497 . . . . . . . . . . 11 ((:ω⟶𝑆𝑘 ∈ ω) → dom (‘suc 𝑘) ∈ ω)
355 nnord 7863 . . . . . . . . . . 11 (dom (‘suc 𝑘) ∈ ω → Ord dom (‘suc 𝑘))
356 ordtr 6379 . . . . . . . . . . 11 (Ord dom (‘suc 𝑘) → Tr dom (‘suc 𝑘))
357 trsuc 6452 . . . . . . . . . . . 12 ((Tr dom (‘suc 𝑘) ∧ suc 𝑘 ∈ dom (‘suc 𝑘)) → 𝑘 ∈ dom (‘suc 𝑘))
358357ex 414 . . . . . . . . . . 11 (Tr dom (‘suc 𝑘) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
359354, 355, 356, 3584syl 19 . . . . . . . . . 10 ((:ω⟶𝑆𝑘 ∈ ω) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
360359adantlr 714 . . . . . . . . 9 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
361307, 360mpd 15 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom (‘suc 𝑘))
362 funssfv 6913 . . . . . . . 8 ((Fun ran ∧ (‘suc 𝑘) ⊆ ran 𝑘 ∈ dom (‘suc 𝑘)) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
363340, 343, 361, 362syl3anc 1372 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
364 simpl 484 . . . . . . . 8 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
365 simpr 486 . . . . . . . . 9 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
366365fveq2d 6896 . . . . . . . 8 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → (𝐹‘( ran 𝑘)) = (𝐹‘((‘suc 𝑘)‘𝑘)))
367364, 366eleq12d 2828 . . . . . . 7 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → (( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)) ↔ ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
368345, 363, 367syl2anc 585 . . . . . 6 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)) ↔ ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
369339, 368mpbird 257 . . . . 5 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))
370369ex 414 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑘 ∈ ω → ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
371293, 370ralrimi 3255 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))
372 vex 3479 . . . . . 6 ∈ V
373372rnex 7903 . . . . 5 ran ∈ V
374373uniex 7731 . . . 4 ran ∈ V
375 feq1 6699 . . . . 5 (𝑔 = ran → (𝑔:ω⟶𝐴 ran :ω⟶𝐴))
376 fveq1 6891 . . . . . 6 (𝑔 = ran → (𝑔‘∅) = ( ran ‘∅))
377376eqeq1d 2735 . . . . 5 (𝑔 = ran → ((𝑔‘∅) = 𝐶 ↔ ( ran ‘∅) = 𝐶))
378 fveq1 6891 . . . . . . 7 (𝑔 = ran → (𝑔‘suc 𝑘) = ( ran ‘suc 𝑘))
379 fveq1 6891 . . . . . . . 8 (𝑔 = ran → (𝑔𝑘) = ( ran 𝑘))
380379fveq2d 6896 . . . . . . 7 (𝑔 = ran → (𝐹‘(𝑔𝑘)) = (𝐹‘( ran 𝑘)))
381378, 380eleq12d 2828 . . . . . 6 (𝑔 = ran → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
382381ralbidv 3178 . . . . 5 (𝑔 = ran → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
383375, 377, 3823anbi123d 1437 . . . 4 (𝑔 = ran → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))) ↔ ( ran :ω⟶𝐴 ∧ ( ran ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))))
384374, 383spcev 3597 . . 3 (( ran :ω⟶𝐴 ∧ ( ran ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
385268, 290, 371, 384syl3anc 1372 . 2 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
386385exlimiv 1934 1 (∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wo 846  w3o 1087  w3a 1088   = wceq 1542  wex 1782  wcel 2107  {cab 2710  wral 3062  wrex 3071  {crab 3433  Vcvv 3475  wss 3949  c0 4323  cop 4635   cuni 4909   ciun 4998  cmpt 5232  Tr wtr 5266  dom cdm 5677  ran crn 5678  cres 5679  Ord word 6364  suc csuc 6367  Fun wfun 6538   Fn wfn 6539  wf 6540  cfv 6544  ωcom 7855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-dc 10441
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-om 7856  df-1o 8466
This theorem is referenced by:  axdc3lem4  10448
  Copyright terms: Public domain W3C validator