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

Theorem axdc3lem2 9862
Description: Lemma for axdc3 9865. 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 9857 (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 9857 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 6667 . . . . . . . . . . . . . 14 (𝑚 = ∅ → (𝑚) = (‘∅))
32dmeqd 5773 . . . . . . . . . . . . 13 (𝑚 = ∅ → dom (𝑚) = dom (‘∅))
41, 3eleq12d 2912 . . . . . . . . . . . 12 (𝑚 = ∅ → (𝑚 ∈ dom (𝑚) ↔ ∅ ∈ dom (‘∅)))
5 eleq2 2906 . . . . . . . . . . . . 13 (𝑚 = ∅ → (𝑗𝑚𝑗 ∈ ∅))
62sseq2d 4003 . . . . . . . . . . . . 13 (𝑚 = ∅ → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (‘∅)))
75, 6imbi12d 346 . . . . . . . . . . . 12 (𝑚 = ∅ → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
84, 7anbi12d 630 . . . . . . . . . . 11 (𝑚 = ∅ → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅)))))
9 id 22 . . . . . . . . . . . . 13 (𝑚 = 𝑖𝑚 = 𝑖)
10 fveq2 6667 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → (𝑚) = (𝑖))
1110dmeqd 5773 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → dom (𝑚) = dom (𝑖))
129, 11eleq12d 2912 . . . . . . . . . . . 12 (𝑚 = 𝑖 → (𝑚 ∈ dom (𝑚) ↔ 𝑖 ∈ dom (𝑖)))
13 elequ2 2122 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → (𝑗𝑚𝑗𝑖))
1410sseq2d 4003 . . . . . . . . . . . . 13 (𝑚 = 𝑖 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑖)))
1513, 14imbi12d 346 . . . . . . . . . . . 12 (𝑚 = 𝑖 → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗𝑖 → (𝑗) ⊆ (𝑖))))
1612, 15anbi12d 630 . . . . . . . . . . 11 (𝑚 = 𝑖 → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖)))))
17 id 22 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖𝑚 = suc 𝑖)
18 fveq2 6667 . . . . . . . . . . . . . 14 (𝑚 = suc 𝑖 → (𝑚) = (‘suc 𝑖))
1918dmeqd 5773 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → dom (𝑚) = dom (‘suc 𝑖))
2017, 19eleq12d 2912 . . . . . . . . . . . 12 (𝑚 = suc 𝑖 → (𝑚 ∈ dom (𝑚) ↔ suc 𝑖 ∈ dom (‘suc 𝑖)))
21 eleq2 2906 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → (𝑗𝑚𝑗 ∈ suc 𝑖))
2218sseq2d 4003 . . . . . . . . . . . . 13 (𝑚 = suc 𝑖 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (‘suc 𝑖)))
2321, 22imbi12d 346 . . . . . . . . . . . 12 (𝑚 = suc 𝑖 → ((𝑗𝑚 → (𝑗) ⊆ (𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))
2420, 23anbi12d 630 . . . . . . . . . . 11 (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))) ↔ (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
25 peano1 7589 . . . . . . . . . . . . . . 15 ∅ ∈ ω
26 ffvelrn 6845 . . . . . . . . . . . . . . 15 ((:ω⟶𝑆 ∧ ∅ ∈ ω) → (‘∅) ∈ 𝑆)
2725, 26mpan2 687 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (‘∅) ∈ 𝑆)
28 axdc3lem2.2 . . . . . . . . . . . . . . . . . 18 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
29 fdm 6519 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠:suc 𝑛𝐴 → dom 𝑠 = suc 𝑛)
30 nnord 7576 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ω → Ord 𝑛)
31 0elsuc 7538 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ord 𝑛 → ∅ ∈ suc 𝑛)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → ∅ ∈ suc 𝑛)
33 peano2 7590 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → suc 𝑛 ∈ ω)
34 eleq2 2906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛))
35 eleq1 2905 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω))
3634, 35anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom 𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω)))
3736biimprcd 251 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
3832, 33, 37syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ω → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
3929, 38syl5com 31 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠:suc 𝑛𝐴 → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
40393ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
4140impcom 408 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
4241rexlimiva 3286 . . . . . . . . . . . . . . . . . . 19 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
4342ss2abi 4047 . . . . . . . . . . . . . . . . . 18 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
4428, 43eqsstri 4005 . . . . . . . . . . . . . . . . 17 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
4544sseli 3967 . . . . . . . . . . . . . . . 16 ((‘∅) ∈ 𝑆 → (‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
46 fvex 6680 . . . . . . . . . . . . . . . . 17 (‘∅) ∈ V
47 dmeq 5771 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (‘∅) → dom 𝑠 = dom (‘∅))
4847eleq2d 2903 . . . . . . . . . . . . . . . . . 18 (𝑠 = (‘∅) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (‘∅)))
4947eleq1d 2902 . . . . . . . . . . . . . . . . . 18 (𝑠 = (‘∅) → (dom 𝑠 ∈ ω ↔ dom (‘∅) ∈ ω))
5048, 49anbi12d 630 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘∅) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω)))
5146, 50elab 3671 . . . . . . . . . . . . . . . 16 ((‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω))
5245, 51sylib 219 . . . . . . . . . . . . . . 15 ((‘∅) ∈ 𝑆 → (∅ ∈ dom (‘∅) ∧ dom (‘∅) ∈ ω))
5352simpld 495 . . . . . . . . . . . . . 14 ((‘∅) ∈ 𝑆 → ∅ ∈ dom (‘∅))
5427, 53syl 17 . . . . . . . . . . . . 13 (:ω⟶𝑆 → ∅ ∈ dom (‘∅))
55 noel 4300 . . . . . . . . . . . . . 14 ¬ 𝑗 ∈ ∅
5655pm2.21i 119 . . . . . . . . . . . . 13 (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))
5754, 56jctir 521 . . . . . . . . . . . 12 (:ω⟶𝑆 → (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
5857adantr 481 . . . . . . . . . . 11 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (∅ ∈ dom (‘∅) ∧ (𝑗 ∈ ∅ → (𝑗) ⊆ (‘∅))))
59 ffvelrn 6845 . . . . . . . . . . . . . . 15 ((:ω⟶𝑆𝑖 ∈ ω) → (𝑖) ∈ 𝑆)
6059ancoms 459 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ :ω⟶𝑆) → (𝑖) ∈ 𝑆)
6160adantrr 713 . . . . . . . . . . . . 13 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑖) ∈ 𝑆)
62 suceq 6254 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
6362fveq2d 6671 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (‘suc 𝑘) = (‘suc 𝑖))
64 2fveq3 6672 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (𝐺‘(𝑘)) = (𝐺‘(𝑖)))
6563, 64eleq12d 2912 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((‘suc 𝑘) ∈ (𝐺‘(𝑘)) ↔ (‘suc 𝑖) ∈ (𝐺‘(𝑖))))
6665rspcva 3625 . . . . . . . . . . . . . 14 ((𝑖 ∈ ω ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘suc 𝑖) ∈ (𝐺‘(𝑖)))
6766adantrl 712 . . . . . . . . . . . . 13 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (‘suc 𝑖) ∈ (𝐺‘(𝑖)))
6844sseli 3967 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ 𝑆 → (𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
69 fvex 6680 . . . . . . . . . . . . . . . . . . . . 21 (𝑖) ∈ V
70 dmeq 5771 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑖) → dom 𝑠 = dom (𝑖))
7170eleq2d 2903 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (𝑖)))
7270eleq1d 2902 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑖) → (dom 𝑠 ∈ ω ↔ dom (𝑖) ∈ ω))
7371, 72anbi12d 630 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω)))
7469, 73elab 3671 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω))
7568, 74sylib 219 . . . . . . . . . . . . . . . . . . 19 ((𝑖) ∈ 𝑆 → (∅ ∈ dom (𝑖) ∧ dom (𝑖) ∈ ω))
7675simprd 496 . . . . . . . . . . . . . . . . . 18 ((𝑖) ∈ 𝑆 → dom (𝑖) ∈ ω)
77 nnord 7576 . . . . . . . . . . . . . . . . . 18 (dom (𝑖) ∈ ω → Ord dom (𝑖))
78 ordsucelsuc 7525 . . . . . . . . . . . . . . . . . 18 (Ord dom (𝑖) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
7976, 77, 783syl 18 . . . . . . . . . . . . . . . . 17 ((𝑖) ∈ 𝑆 → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
8079adantr 481 . . . . . . . . . . . . . . . 16 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
81 dmeq 5771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑖) → dom 𝑥 = dom (𝑖))
82 suceq 6254 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑥 = dom (𝑖) → suc dom 𝑥 = suc dom (𝑖))
8381, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → suc dom 𝑥 = suc dom (𝑖))
8483eqeq2d 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (𝑖)))
8581reseq2d 5852 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (𝑖)))
86 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑖) → 𝑥 = (𝑖))
8785, 86eqeq12d 2842 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (𝑖)) = (𝑖)))
8884, 87anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑖) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))))
8988rabbidv 3486 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑖) → {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))})
90 axdc3lem2.3 . . . . . . . . . . . . . . . . . . . . . 22 𝐺 = (𝑥𝑆 ↦ {𝑦𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
91 axdc3lem2.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝐴 ∈ V
9291, 28axdc3lem 9861 . . . . . . . . . . . . . . . . . . . . . . 23 𝑆 ∈ V
9392rabex 5232 . . . . . . . . . . . . . . . . . . . . . 22 {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))} ∈ V
9489, 90, 93fvmpt 6765 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖) ∈ 𝑆 → (𝐺‘(𝑖)) = {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))})
9594eleq2d 2903 . . . . . . . . . . . . . . . . . . . 20 ((𝑖) ∈ 𝑆 → ((‘suc 𝑖) ∈ (𝐺‘(𝑖)) ↔ (‘suc 𝑖) ∈ {𝑦𝑆 ∣ (dom 𝑦 = suc dom (𝑖) ∧ (𝑦 ↾ dom (𝑖)) = (𝑖))}))
96 dmeq 5771 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (‘suc 𝑖) → dom 𝑦 = dom (‘suc 𝑖))
9796eqeq1d 2828 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (‘suc 𝑖) → (dom 𝑦 = suc dom (𝑖) ↔ dom (‘suc 𝑖) = suc dom (𝑖)))
98 reseq1 5846 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (‘suc 𝑖) → (𝑦 ↾ dom (𝑖)) = ((‘suc 𝑖) ↾ dom (𝑖)))
9998eqeq1d 2828 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (‘suc 𝑖) → ((𝑦 ↾ dom (𝑖)) = (𝑖) ↔ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))
10097, 99anbi12d 630 . . . . . . . . . . . . . . . . . . . . 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, 101syl6bb 288 . . . . . . . . . . . . . . . . . . 19 ((𝑖) ∈ 𝑆 → ((‘suc 𝑖) ∈ (𝐺‘(𝑖)) ↔ ((‘suc 𝑖) ∈ 𝑆 ∧ (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))))
103102simplbda 500 . . . . . . . . . . . . . . . . . 18 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (dom (‘suc 𝑖) = suc dom (𝑖) ∧ ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖)))
104103simpld 495 . . . . . . . . . . . . . . . . 17 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → dom (‘suc 𝑖) = suc dom (𝑖))
105104eleq2d 2903 . . . . . . . . . . . . . . . 16 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (𝑖)))
10680, 105bitr4d 283 . . . . . . . . . . . . . . 15 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) ↔ suc 𝑖 ∈ dom (‘suc 𝑖)))
107106biimpd 230 . . . . . . . . . . . . . 14 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → (𝑖 ∈ dom (𝑖) → suc 𝑖 ∈ dom (‘suc 𝑖)))
108103simprd 496 . . . . . . . . . . . . . . 15 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → ((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖))
109 resss 5877 . . . . . . . . . . . . . . . 16 ((‘suc 𝑖) ↾ dom (𝑖)) ⊆ (‘suc 𝑖)
110 sseq1 3996 . . . . . . . . . . . . . . . 16 (((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖) → (((‘suc 𝑖) ↾ dom (𝑖)) ⊆ (‘suc 𝑖) ↔ (𝑖) ⊆ (‘suc 𝑖)))
111109, 110mpbii 234 . . . . . . . . . . . . . . 15 (((‘suc 𝑖) ↾ dom (𝑖)) = (𝑖) → (𝑖) ⊆ (‘suc 𝑖))
112 elsuci 6255 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ suc 𝑖 → (𝑗𝑖𝑗 = 𝑖))
113 pm2.27 42 . . . . . . . . . . . . . . . . . . 19 (𝑗𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → (𝑗) ⊆ (𝑖)))
114 sstr2 3978 . . . . . . . . . . . . . . . . . . 19 ((𝑗) ⊆ (𝑖) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖)))
115113, 114syl6 35 . . . . . . . . . . . . . . . . . 18 (𝑗𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
116 fveq2 6667 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝑗) = (𝑖))
117116sseq1d 4002 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → ((𝑗) ⊆ (‘suc 𝑖) ↔ (𝑖) ⊆ (‘suc 𝑖)))
118117biimprd 249 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖)))
119118a1d 25 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝑗𝑖 → (𝑗) ⊆ (𝑖)) → ((𝑖) ⊆ (‘suc 𝑖) → (𝑗) ⊆ (‘suc 𝑖))))
120115, 119jaoi 853 . . . . . . . . . . . . . . . . 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 608 . . . . . . . . . . . . 13 (((𝑖) ∈ 𝑆 ∧ (‘suc 𝑖) ∈ (𝐺‘(𝑖))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
12561, 67, 124syl2anc 584 . . . . . . . . . . . 12 ((𝑖 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖)))))
126125ex 413 . . . . . . . . . . 11 (𝑖 ∈ ω → ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((𝑖 ∈ dom (𝑖) ∧ (𝑗𝑖 → (𝑗) ⊆ (𝑖))) → (suc 𝑖 ∈ dom (‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (𝑗) ⊆ (‘suc 𝑖))))))
1278, 16, 24, 58, 126finds2 7598 . . . . . . . . . 10 (𝑚 ∈ ω → ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚)))))
128127imp 407 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑚 ∈ dom (𝑚) ∧ (𝑗𝑚 → (𝑗) ⊆ (𝑚))))
129128simprd 496 . . . . . . . 8 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑗𝑚 → (𝑗) ⊆ (𝑚)))
130129expcom 414 . . . . . . 7 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → (𝑗𝑚 → (𝑗) ⊆ (𝑚))))
131130ralrimdv 3193 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → ∀𝑗𝑚 (𝑗) ⊆ (𝑚)))
132131ralrimiv 3186 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚))
133 frn 6517 . . . . . . . . . . . 12 (:ω⟶𝑆 → ran 𝑆)
134 ffun 6514 . . . . . . . . . . . . . . . 16 (𝑠:suc 𝑛𝐴 → Fun 𝑠)
1351343ad2ant1 1127 . . . . . . . . . . . . . . 15 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → Fun 𝑠)
136135rexlimivw 3287 . . . . . . . . . . . . . 14 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → Fun 𝑠)
137136ss2abi 4047 . . . . . . . . . . . . 13 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠}
13828, 137eqsstri 4005 . . . . . . . . . . . 12 𝑆 ⊆ {𝑠 ∣ Fun 𝑠}
139133, 138syl6ss 3983 . . . . . . . . . . 11 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ Fun 𝑠})
140139sseld 3970 . . . . . . . . . 10 (:ω⟶𝑆 → (𝑢 ∈ ran 𝑢 ∈ {𝑠 ∣ Fun 𝑠}))
141 vex 3503 . . . . . . . . . . 11 𝑢 ∈ V
142 funeq 6372 . . . . . . . . . . 11 (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢))
143141, 142elab 3671 . . . . . . . . . 10 (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢)
144140, 143syl6ib 252 . . . . . . . . 9 (:ω⟶𝑆 → (𝑢 ∈ ran → Fun 𝑢))
145144adantr 481 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → Fun 𝑢))
146 ffn 6511 . . . . . . . . 9 (:ω⟶𝑆 Fn ω)
147 fvelrnb 6723 . . . . . . . . . . . . 13 ( Fn ω → (𝑣 ∈ ran ↔ ∃𝑏 ∈ ω (𝑏) = 𝑣))
148 fvelrnb 6723 . . . . . . . . . . . . . . 15 ( Fn ω → (𝑢 ∈ ran ↔ ∃𝑎 ∈ ω (𝑎) = 𝑢))
149 nnord 7576 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ω → Ord 𝑎)
150 nnord 7576 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ ω → Ord 𝑏)
151149, 150anim12i 612 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord 𝑎 ∧ Ord 𝑏))
152 ordtri3or 6221 . . . . . . . . . . . . . . . . . . . . . . 23 ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎𝑏𝑎 = 𝑏𝑏𝑎))
153 fveq2 6667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑏 → (𝑚) = (𝑏))
154153sseq2d 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑏 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑏)))
155154raleqbi1dv 3409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 = 𝑏 → (∀𝑗𝑚 (𝑗) ⊆ (𝑚) ↔ ∀𝑗𝑏 (𝑗) ⊆ (𝑏)))
156155rspcv 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ∀𝑗𝑏 (𝑗) ⊆ (𝑏)))
157 fveq2 6667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑎 → (𝑗) = (𝑎))
158157sseq1d 4002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑎 → ((𝑗) ⊆ (𝑏) ↔ (𝑎) ⊆ (𝑏)))
159158rspccv 3624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑗𝑏 (𝑗) ⊆ (𝑏) → (𝑎𝑏 → (𝑎) ⊆ (𝑏)))
160156, 159syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → (𝑎) ⊆ (𝑏))))
161160adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → (𝑎) ⊆ (𝑏))))
1621613imp 1105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑎𝑏) → (𝑎) ⊆ (𝑏))
163162orcd 871 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑎𝑏) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1641633exp 1113 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑎𝑏 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
165164com3r 87 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
166 fveq2 6667 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑏 → (𝑎) = (𝑏))
167 eqimss 4027 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎) = (𝑏) → (𝑎) ⊆ (𝑏))
168167orcd 871 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎) = (𝑏) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
169166, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑏 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1701692a1d 26 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
171 fveq2 6667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑎 → (𝑚) = (𝑎))
172171sseq2d 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑎 → ((𝑗) ⊆ (𝑚) ↔ (𝑗) ⊆ (𝑎)))
173172raleqbi1dv 3409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 = 𝑎 → (∀𝑗𝑚 (𝑗) ⊆ (𝑚) ↔ ∀𝑗𝑎 (𝑗) ⊆ (𝑎)))
174173rspcv 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ∀𝑗𝑎 (𝑗) ⊆ (𝑎)))
175 fveq2 6667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑏 → (𝑗) = (𝑏))
176175sseq1d 4002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑏 → ((𝑗) ⊆ (𝑎) ↔ (𝑏) ⊆ (𝑎)))
177176rspccv 3624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑗𝑎 (𝑗) ⊆ (𝑎) → (𝑏𝑎 → (𝑏) ⊆ (𝑎)))
178174, 177syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → (𝑏) ⊆ (𝑎))))
179178adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → (𝑏) ⊆ (𝑎))))
1801793imp 1105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑏𝑎) → (𝑏) ⊆ (𝑎))
181180olcd 872 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) ∧ 𝑏𝑎) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))
1821813exp 1113 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑏𝑎 → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
183182com3r 87 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
184165, 170, 1833jaoi 1421 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝑏𝑎 = 𝑏𝑏𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
185152, 184syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((Ord 𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)))))
186151, 185mpcom 38 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → ((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎))))
187 sseq12 3998 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → ((𝑎) ⊆ (𝑏) ↔ 𝑢𝑣))
188 sseq12 3998 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑏) = 𝑣 ∧ (𝑎) = 𝑢) → ((𝑏) ⊆ (𝑎) ↔ 𝑣𝑢))
189188ancoms 459 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → ((𝑏) ⊆ (𝑎) ↔ 𝑣𝑢))
190187, 189orbi12d 914 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)) ↔ (𝑢𝑣𝑣𝑢)))
191190biimpcd 250 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎) ⊆ (𝑏) ∨ (𝑏) ⊆ (𝑎)) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (𝑢𝑣𝑣𝑢)))
192186, 191syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (𝑢𝑣𝑣𝑢))))
193192com23 86 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((𝑎) = 𝑢 ∧ (𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))
194193exp4b 431 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ω → (𝑏 ∈ ω → ((𝑎) = 𝑢 → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))))
195194com23 86 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ω → ((𝑎) = 𝑢 → (𝑏 ∈ ω → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))))
196195rexlimiv 3285 . . . . . . . . . . . . . . . 16 (∃𝑎 ∈ ω (𝑎) = 𝑢 → (𝑏 ∈ ω → ((𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
197196rexlimdv 3288 . . . . . . . . . . . . . . 15 (∃𝑎 ∈ ω (𝑎) = 𝑢 → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢))))
198148, 197syl6bi 254 . . . . . . . . . . . . . 14 ( Fn ω → (𝑢 ∈ ran → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
199198com23 86 . . . . . . . . . . . . 13 ( Fn ω → (∃𝑏 ∈ ω (𝑏) = 𝑣 → (𝑢 ∈ ran → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
200147, 199sylbid 241 . . . . . . . . . . . 12 ( Fn ω → (𝑣 ∈ ran → (𝑢 ∈ ran → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢𝑣𝑣𝑢)))))
201200com24 95 . . . . . . . . . . 11 ( Fn ω → (∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚) → (𝑢 ∈ ran → (𝑣 ∈ ran → (𝑢𝑣𝑣𝑢)))))
202201imp 407 . . . . . . . . . 10 (( Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → (𝑣 ∈ ran → (𝑢𝑣𝑣𝑢))))
203202ralrimdv 3193 . . . . . . . . 9 (( Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
204146, 203sylan 580 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
205145, 204jcad 513 . . . . . . 7 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → (𝑢 ∈ ran → (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢))))
206205ralrimiv 3186 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → ∀𝑢 ∈ ran (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)))
207 fununi 6426 . . . . . 6 (∀𝑢 ∈ ran (Fun 𝑢 ∧ ∀𝑣 ∈ ran (𝑢𝑣𝑣𝑢)) → Fun ran )
208206, 207syl 17 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗𝑚 (𝑗) ⊆ (𝑚)) → Fun ran )
209132, 208syldan 591 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → Fun ran )
210 vex 3503 . . . . . . . . 9 𝑚 ∈ V
211210eldm2 5769 . . . . . . . 8 (𝑚 ∈ dom ran ↔ ∃𝑢𝑚, 𝑢⟩ ∈ ran )
212 eluni2 4841 . . . . . . . . . 10 (⟨𝑚, 𝑢⟩ ∈ ran ↔ ∃𝑣 ∈ ran 𝑚, 𝑢⟩ ∈ 𝑣)
213210, 141opeldm 5775 . . . . . . . . . . . . . . 15 (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ dom 𝑣)
214213a1i 11 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ dom 𝑣))
215133, 44syl6ss 3983 . . . . . . . . . . . . . . 15 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
216 ssel 3965 . . . . . . . . . . . . . . . 16 (ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
217 vex 3503 . . . . . . . . . . . . . . . . . 18 𝑣 ∈ V
218 dmeq 5771 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣)
219218eleq2d 2903 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣))
220218eleq1d 2902 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω))
221219, 220anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
222217, 221elab 3671 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))
223222simprbi 497 . . . . . . . . . . . . . . . 16 (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → dom 𝑣 ∈ ω)
224216, 223syl6 35 . . . . . . . . . . . . . . 15 (ran ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran → dom 𝑣 ∈ ω))
225215, 224syl 17 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → (𝑣 ∈ ran → dom 𝑣 ∈ ω))
226214, 225anim12d 608 . . . . . . . . . . . . 13 (:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣𝑣 ∈ ran ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
227 elnn 7578 . . . . . . . . . . . . 13 ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω)
228226, 227syl6 35 . . . . . . . . . . . 12 (:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣𝑣 ∈ ran ) → 𝑚 ∈ ω))
229228expcomd 417 . . . . . . . . . . 11 (:ω⟶𝑆 → (𝑣 ∈ ran → (⟨𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ ω)))
230229rexlimdv 3288 . . . . . . . . . 10 (:ω⟶𝑆 → (∃𝑣 ∈ ran 𝑚, 𝑢⟩ ∈ 𝑣𝑚 ∈ ω))
231212, 230syl5bi 243 . . . . . . . . 9 (:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ ran 𝑚 ∈ ω))
232231exlimdv 1927 . . . . . . . 8 (:ω⟶𝑆 → (∃𝑢𝑚, 𝑢⟩ ∈ ran 𝑚 ∈ ω))
233211, 232syl5bi 243 . . . . . . 7 (:ω⟶𝑆 → (𝑚 ∈ dom ran 𝑚 ∈ ω))
234233adantr 481 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom ran 𝑚 ∈ ω))
235 id 22 . . . . . . . . . . 11 (𝑚 ∈ ω → 𝑚 ∈ ω)
236 fnfvelrn 6844 . . . . . . . . . . 11 (( Fn ω ∧ 𝑚 ∈ ω) → (𝑚) ∈ ran )
237146, 235, 236syl2anr 596 . . . . . . . . . 10 ((𝑚 ∈ ω ∧ :ω⟶𝑆) → (𝑚) ∈ ran )
238237adantrr 713 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → (𝑚) ∈ ran )
239128simpld 495 . . . . . . . . 9 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 ∈ dom (𝑚))
240 dmeq 5771 . . . . . . . . . 10 (𝑢 = (𝑚) → dom 𝑢 = dom (𝑚))
241240eliuni 4923 . . . . . . . . 9 (((𝑚) ∈ ran 𝑚 ∈ dom (𝑚)) → 𝑚 𝑢 ∈ ran dom 𝑢)
242238, 239, 241syl2anc 584 . . . . . . . 8 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 𝑢 ∈ ran dom 𝑢)
243 dmuni 5782 . . . . . . . 8 dom ran = 𝑢 ∈ ran dom 𝑢
244242, 243syl6eleqr 2929 . . . . . . 7 ((𝑚 ∈ ω ∧ (:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))) → 𝑚 ∈ dom ran )
245244expcom 414 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ran ))
246234, 245impbid 213 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ dom ran 𝑚 ∈ ω))
247246eqrdv 2824 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → dom ran = ω)
248 rnuni 6005 . . . . . 6 ran ran = 𝑠 ∈ ran ran 𝑠
249 frn 6517 . . . . . . . . . . . . . 14 (𝑠:suc 𝑛𝐴 → ran 𝑠𝐴)
2502493ad2ant1 1127 . . . . . . . . . . . . 13 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → ran 𝑠𝐴)
251250rexlimivw 3287 . . . . . . . . . . . 12 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → ran 𝑠𝐴)
252251ss2abi 4047 . . . . . . . . . . 11 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ ran 𝑠𝐴}
25328, 252eqsstri 4005 . . . . . . . . . 10 𝑆 ⊆ {𝑠 ∣ ran 𝑠𝐴}
254133, 253syl6ss 3983 . . . . . . . . 9 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ ran 𝑠𝐴})
255 ssel 3965 . . . . . . . . . 10 (ran ⊆ {𝑠 ∣ ran 𝑠𝐴} → (𝑠 ∈ ran 𝑠 ∈ {𝑠 ∣ ran 𝑠𝐴}))
256 abid 2808 . . . . . . . . . 10 (𝑠 ∈ {𝑠 ∣ ran 𝑠𝐴} ↔ ran 𝑠𝐴)
257255, 256syl6ib 252 . . . . . . . . 9 (ran ⊆ {𝑠 ∣ ran 𝑠𝐴} → (𝑠 ∈ ran → ran 𝑠𝐴))
258254, 257syl 17 . . . . . . . 8 (:ω⟶𝑆 → (𝑠 ∈ ran → ran 𝑠𝐴))
259258ralrimiv 3186 . . . . . . 7 (:ω⟶𝑆 → ∀𝑠 ∈ ran ran 𝑠𝐴)
260 iunss 4966 . . . . . . 7 ( 𝑠 ∈ ran ran 𝑠𝐴 ↔ ∀𝑠 ∈ ran ran 𝑠𝐴)
261259, 260sylibr 235 . . . . . 6 (:ω⟶𝑆 𝑠 ∈ ran ran 𝑠𝐴)
262248, 261eqsstrid 4019 . . . . 5 (:ω⟶𝑆 → ran ran 𝐴)
263262adantr 481 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ran ran 𝐴)
264 df-fn 6355 . . . . 5 ( ran Fn ω ↔ (Fun ran ∧ dom ran = ω))
265 df-f 6356 . . . . . 6 ( ran :ω⟶𝐴 ↔ ( ran Fn ω ∧ ran ran 𝐴))
266265biimpri 229 . . . . 5 (( ran Fn ω ∧ ran ran 𝐴) → ran :ω⟶𝐴)
267264, 266sylanbr 582 . . . 4 (((Fun ran ∧ dom ran = ω) ∧ ran ran 𝐴) → ran :ω⟶𝐴)
268209, 247, 263, 267syl21anc 835 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ran :ω⟶𝐴)
269 fnfvelrn 6844 . . . . . . . 8 (( Fn ω ∧ ∅ ∈ ω) → (‘∅) ∈ ran )
270146, 25, 269sylancl 586 . . . . . . 7 (:ω⟶𝑆 → (‘∅) ∈ ran )
271270adantr 481 . . . . . 6 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘∅) ∈ ran )
272 elssuni 4866 . . . . . 6 ((‘∅) ∈ ran → (‘∅) ⊆ ran )
273271, 272syl 17 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (‘∅) ⊆ ran )
27454adantr 481 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∅ ∈ dom (‘∅))
275 funssfv 6688 . . . . 5 ((Fun ran ∧ (‘∅) ⊆ ran ∧ ∅ ∈ dom (‘∅)) → ( ran ‘∅) = ((‘∅)‘∅))
276209, 273, 274, 275syl3anc 1365 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ( ran ‘∅) = ((‘∅)‘∅))
277 simp2 1131 . . . . . . . . . . 11 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑠‘∅) = 𝐶)
278277rexlimivw 3287 . . . . . . . . . 10 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑠‘∅) = 𝐶)
279278ss2abi 4047 . . . . . . . . 9 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
28028, 279eqsstri 4005 . . . . . . . 8 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
281133, 280syl6ss 3983 . . . . . . 7 (:ω⟶𝑆 → ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶})
282 ssel 3965 . . . . . . . 8 (ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((‘∅) ∈ ran → (‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶}))
283 fveq1 6666 . . . . . . . . . 10 (𝑠 = (‘∅) → (𝑠‘∅) = ((‘∅)‘∅))
284283eqeq1d 2828 . . . . . . . . 9 (𝑠 = (‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((‘∅)‘∅) = 𝐶))
28546, 284elab 3671 . . . . . . . 8 ((‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((‘∅)‘∅) = 𝐶)
286282, 285syl6ib 252 . . . . . . 7 (ran ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
287281, 286syl 17 . . . . . 6 (:ω⟶𝑆 → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
288287adantr 481 . . . . 5 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((‘∅) ∈ ran → ((‘∅)‘∅) = 𝐶))
289271, 288mpd 15 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ((‘∅)‘∅) = 𝐶)
290276, 289eqtrd 2861 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ( ran ‘∅) = 𝐶)
291 nfv 1908 . . . . 5 𝑘 :ω⟶𝑆
292 nfra1 3224 . . . . 5 𝑘𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))
293291, 292nfan 1893 . . . 4 𝑘(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘)))
294133ad2antrr 722 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ran 𝑆)
295 peano2 7590 . . . . . . . . 9 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
296 fnfvelrn 6844 . . . . . . . . 9 (( Fn ω ∧ suc 𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
297146, 295, 296syl2an 595 . . . . . . . 8 ((:ω⟶𝑆𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
298297adantlr 711 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ∈ ran )
299239expcom 414 . . . . . . . . 9 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (𝑚)))
300299ralrimiv 3186 . . . . . . . 8 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚))
301 id 22 . . . . . . . . . . 11 (𝑚 = suc 𝑘𝑚 = suc 𝑘)
302 fveq2 6667 . . . . . . . . . . . 12 (𝑚 = suc 𝑘 → (𝑚) = (‘suc 𝑘))
303302dmeqd 5773 . . . . . . . . . . 11 (𝑚 = suc 𝑘 → dom (𝑚) = dom (‘suc 𝑘))
304301, 303eleq12d 2912 . . . . . . . . . 10 (𝑚 = suc 𝑘 → (𝑚 ∈ dom (𝑚) ↔ suc 𝑘 ∈ dom (‘suc 𝑘)))
305304rspcv 3622 . . . . . . . . 9 (suc 𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚) → suc 𝑘 ∈ dom (‘suc 𝑘)))
306295, 305syl 17 . . . . . . . 8 (𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (𝑚) → suc 𝑘 ∈ dom (‘suc 𝑘)))
307300, 306mpan9 507 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (‘suc 𝑘))
308 eleq2 2906 . . . . . . . . . . . . . . . . . . . . 21 (dom 𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛))
309308biimpa 477 . . . . . . . . . . . . . . . . . . . 20 ((dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
31029, 309sylan 580 . . . . . . . . . . . . . . . . . . 19 ((𝑠:suc 𝑛𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
311 ordsucelsuc 7525 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord 𝑛 → (𝑘𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
31230, 311syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ω → (𝑘𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
313312biimprd 249 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛𝑘𝑛))
314 rsp 3210 . . . . . . . . . . . . . . . . . . . . 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 413 . . . . . . . . . . . . . . . . 17 (𝑠:suc 𝑛𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))))
319318com24 95 . . . . . . . . . . . . . . . 16 (𝑠:suc 𝑛𝐴 → (∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))))
320319imp 407 . . . . . . . . . . . . . . 15 ((𝑠:suc 𝑛𝐴 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
3213203adant2 1125 . . . . . . . . . . . . . 14 ((𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))))
322321impcom 408 . . . . . . . . . . . . 13 ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))
323322rexlimiva 3286 . . . . . . . . . . . 12 (∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))))
324323ss2abi 4047 . . . . . . . . . . 11 {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
32528, 324eqsstri 4005 . . . . . . . . . 10 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}
326 sstr 3979 . . . . . . . . . 10 ((ran 𝑆𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}) → ran ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))})
327325, 326mpan2 687 . . . . . . . . 9 (ran 𝑆 → ran ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))})
328327sseld 3970 . . . . . . . 8 (ran 𝑆 → ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))}))
329 fvex 6680 . . . . . . . . 9 (‘suc 𝑘) ∈ V
330 dmeq 5771 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → dom 𝑠 = dom (‘suc 𝑘))
331330eleq2d 2903 . . . . . . . . . 10 (𝑠 = (‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (‘suc 𝑘)))
332 fveq1 6666 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → (𝑠‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
333 fveq1 6666 . . . . . . . . . . . 12 (𝑠 = (‘suc 𝑘) → (𝑠𝑘) = ((‘suc 𝑘)‘𝑘))
334333fveq2d 6671 . . . . . . . . . . 11 (𝑠 = (‘suc 𝑘) → (𝐹‘(𝑠𝑘)) = (𝐹‘((‘suc 𝑘)‘𝑘)))
335332, 334eleq12d 2912 . . . . . . . . . 10 (𝑠 = (‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)) ↔ ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
336331, 335imbi12d 346 . . . . . . . . 9 (𝑠 = (‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘))) ↔ (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))))
337329, 336elab 3671 . . . . . . . 8 ((‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠𝑘)))} ↔ (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘))))
338328, 337syl6ib 252 . . . . . . 7 (ran 𝑆 → ((‘suc 𝑘) ∈ ran → (suc 𝑘 ∈ dom (‘suc 𝑘) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))))
339294, 298, 307, 338syl3c 66 . . . . . 6 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ((‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((‘suc 𝑘)‘𝑘)))
340209adantr 481 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → Fun ran )
341 elssuni 4866 . . . . . . . . . 10 ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ⊆ ran )
342297, 341syl 17 . . . . . . . . 9 ((:ω⟶𝑆𝑘 ∈ ω) → (‘suc 𝑘) ⊆ ran )
343342adantlr 711 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (‘suc 𝑘) ⊆ ran )
344 funssfv 6688 . . . . . . . 8 ((Fun ran ∧ (‘suc 𝑘) ⊆ ran ∧ suc 𝑘 ∈ dom (‘suc 𝑘)) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
345340, 343, 307, 344syl3anc 1365 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
346215sseld 3970 . . . . . . . . . . . . . . 15 (:ω⟶𝑆 → ((‘suc 𝑘) ∈ ran → (‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
347330eleq2d 2903 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (‘suc 𝑘)))
348330eleq1d 2902 . . . . . . . . . . . . . . . . 17 (𝑠 = (‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (‘suc 𝑘) ∈ ω))
349347, 348anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑠 = (‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
350329, 349elab 3671 . . . . . . . . . . . . . . 15 ((‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω))
351346, 350syl6ib 252 . . . . . . . . . . . . . 14 (:ω⟶𝑆 → ((‘suc 𝑘) ∈ ran → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
352351adantr 481 . . . . . . . . . . . . 13 ((:ω⟶𝑆𝑘 ∈ ω) → ((‘suc 𝑘) ∈ ran → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω)))
353297, 352mpd 15 . . . . . . . . . . . 12 ((:ω⟶𝑆𝑘 ∈ ω) → (∅ ∈ dom (‘suc 𝑘) ∧ dom (‘suc 𝑘) ∈ ω))
354353simprd 496 . . . . . . . . . . 11 ((:ω⟶𝑆𝑘 ∈ ω) → dom (‘suc 𝑘) ∈ ω)
355 nnord 7576 . . . . . . . . . . 11 (dom (‘suc 𝑘) ∈ ω → Ord dom (‘suc 𝑘))
356 ordtr 6203 . . . . . . . . . . 11 (Ord dom (‘suc 𝑘) → Tr dom (‘suc 𝑘))
357 trsuc 6273 . . . . . . . . . . . 12 ((Tr dom (‘suc 𝑘) ∧ suc 𝑘 ∈ dom (‘suc 𝑘)) → 𝑘 ∈ dom (‘suc 𝑘))
358357ex 413 . . . . . . . . . . 11 (Tr dom (‘suc 𝑘) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
359354, 355, 356, 3584syl 19 . . . . . . . . . 10 ((:ω⟶𝑆𝑘 ∈ ω) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
360359adantlr 711 . . . . . . . . 9 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (‘suc 𝑘) → 𝑘 ∈ dom (‘suc 𝑘)))
361307, 360mpd 15 . . . . . . . 8 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom (‘suc 𝑘))
362 funssfv 6688 . . . . . . . 8 ((Fun ran ∧ (‘suc 𝑘) ⊆ ran 𝑘 ∈ dom (‘suc 𝑘)) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
363340, 343, 361, 362syl3anc 1365 . . . . . . 7 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
364 simpl 483 . . . . . . . 8 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → ( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘))
365 simpr 485 . . . . . . . . 9 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → ( ran 𝑘) = ((‘suc 𝑘)‘𝑘))
366365fveq2d 6671 . . . . . . . 8 ((( ran ‘suc 𝑘) = ((‘suc 𝑘)‘suc 𝑘) ∧ ( ran 𝑘) = ((‘suc 𝑘)‘𝑘)) → (𝐹‘( ran 𝑘)) = (𝐹‘((‘suc 𝑘)‘𝑘)))
367364, 366eleq12d 2912 . . . . . . 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 258 . . . . 5 (((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) ∧ 𝑘 ∈ ω) → ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))
370369ex 413 . . . 4 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → (𝑘 ∈ ω → ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
371293, 370ralrimi 3221 . . 3 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))
372 vex 3503 . . . . . 6 ∈ V
373372rnex 7605 . . . . 5 ran ∈ V
374373uniex 7455 . . . 4 ran ∈ V
375 feq1 6492 . . . . 5 (𝑔 = ran → (𝑔:ω⟶𝐴 ran :ω⟶𝐴))
376 fveq1 6666 . . . . . 6 (𝑔 = ran → (𝑔‘∅) = ( ran ‘∅))
377376eqeq1d 2828 . . . . 5 (𝑔 = ran → ((𝑔‘∅) = 𝐶 ↔ ( ran ‘∅) = 𝐶))
378 fveq1 6666 . . . . . . 7 (𝑔 = ran → (𝑔‘suc 𝑘) = ( ran ‘suc 𝑘))
379 fveq1 6666 . . . . . . . 8 (𝑔 = ran → (𝑔𝑘) = ( ran 𝑘))
380379fveq2d 6671 . . . . . . 7 (𝑔 = ran → (𝐹‘(𝑔𝑘)) = (𝐹‘( ran 𝑘)))
381378, 380eleq12d 2912 . . . . . 6 (𝑔 = ran → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
382381ralbidv 3202 . . . . 5 (𝑔 = ran → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘)) ↔ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))))
383375, 377, 3823anbi123d 1429 . . . 4 (𝑔 = ran → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))) ↔ ( ran :ω⟶𝐴 ∧ ( ran ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘)))))
384374, 383spcev 3611 . . 3 (( ran :ω⟶𝐴 ∧ ( ran ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ( ran ‘suc 𝑘) ∈ (𝐹‘( ran 𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
385268, 290, 371, 384syl3anc 1365 . 2 ((:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
386385exlimiv 1924 1 (∃(:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝐺‘(𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 843  w3o 1080  w3a 1081   = wceq 1530  wex 1773  wcel 2107  {cab 2804  wral 3143  wrex 3144  {crab 3147  Vcvv 3500  wss 3940  c0 4295  cop 4570   cuni 4837   ciun 4917  cmpt 5143  Tr wtr 5169  dom cdm 5554  ran crn 5555  cres 5556  Ord word 6188  suc csuc 6191  Fun wfun 6346   Fn wfn 6347  wf 6348  cfv 6352  ωcom 7568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-dc 9857
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-fv 6360  df-om 7569  df-1o 8093
This theorem is referenced by:  axdc3lem4  9864
  Copyright terms: Public domain W3C validator