Theorem axdc3lem2 10394

Description: Lemma for axdc3 10397. 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 10389 (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 10389 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.

Step	Hyp	Ref	Expression
1		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → 𝑚 = ∅)
2		fveq2 6852	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅))
3	2	dmeqd 5870	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → dom (ℎ‘𝑚) = dom (ℎ‘∅))
4	1, 3	eleq12d 2846	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑚 ∈ dom (ℎ‘𝑚) ↔ ∅ ∈ dom (ℎ‘∅)))
5		eleq2 2841	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ ∅))
6	2	sseq2d 3959	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘∅)))
7	5, 6	imbi12d 346	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
8	4, 7	anbi12d 640	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))))
9		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → 𝑚 = 𝑖)
10		fveq2 6852	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖))
11	10	dmeqd 5870	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘𝑖))
12	9, 11	eleq12d 2846	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ 𝑖 ∈ dom (ℎ‘𝑖)))
13		elequ2 2147	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ 𝑖))
14	10	sseq2d 3959	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))
15	13, 14	imbi12d 346	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))))
16	12, 15	anbi12d 640	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))))
17		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → 𝑚 = suc 𝑖)
18		fveq2 6852	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖))
19	18	dmeqd 5870	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑖))
20	17, 19	eleq12d 2846	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
21		eleq2 2841	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ suc 𝑖))
22	18	sseq2d 3959	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
23	21, 22	imbi12d 346	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
24	20, 23	anbi12d 640	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
25		peano1 7854	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
26		ffvelcdm 7047	. . . . . . . . . . . . . . 15 ⊢ ((ℎ:ω⟶𝑆 ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ 𝑆)
27	25, 26	mpan2 699	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ 𝑆)
28		axdc3lem2.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
29		fdm 6686	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠:suc 𝑛⟶𝐴 → dom 𝑠 = suc 𝑛)
30		nnord 7839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ω → Ord 𝑛)
31		0elsuc 7800	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑛 → ∅ ∈ suc 𝑛)
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → ∅ ∈ suc 𝑛)
33		peano2 7855	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
34		eleq2 2841	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛))
35		eleq1 2840	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω))
36	34, 35	anbi12d 640	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (dom 𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω)))
37	36	biimprcd 252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
38	32, 33, 37	syl2anc 592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
39	29, 38	syl5com 31	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠:suc 𝑛⟶𝐴 → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
40	39	3ad2ant1 1142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
41	40	impcom 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
42	41	rexlimiva 3145	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
43	42	ss2abi 4010	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
44	28, 43	eqsstri 3973	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
45	44	sseli 3923	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘∅) ∈ 𝑆 → (ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
46		fvex 6865	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ‘∅) ∈ V
47		dmeq 5868	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = (ℎ‘∅) → dom 𝑠 = dom (ℎ‘∅))
48	47	eleq2d 2838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (ℎ‘∅) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘∅)))
49	47	eleq1d 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (ℎ‘∅) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘∅) ∈ ω))
50	48, 49	anbi12d 640	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘∅) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω)))
51	46, 50	elab 3629	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω))
52	45, 51	sylib 220	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘∅) ∈ 𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω))
53	52	simpld 497	. . . . . . . . . . . . . 14 ⊢ ((ℎ‘∅) ∈ 𝑆 → ∅ ∈ dom (ℎ‘∅))
54	27, 53	syl 17	. . . . . . . . . . . . 13 ⊢ (ℎ:ω⟶𝑆 → ∅ ∈ dom (ℎ‘∅))
55		noel 4281	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑗 ∈ ∅
56	55	pm2.21i 119	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))
57	54, 56	jctir 527	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
58	57	adantr 483	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
59		ffvelcdm 7047	. . . . . . . . . . . . . . 15 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ 𝑆)
60	59	ancoms 461	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑖) ∈ 𝑆)
61	60	adantrr 725	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑖) ∈ 𝑆)
62		suceq 6399	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
63	62	fveq2d 6856	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
64		2fveq3 6857	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖)))
65	63, 64	eleq12d 2846	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
66	65	rspcva 3570	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))
67	66	adantrl 724	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))
68	44	sseli 3923	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
69		fvex 6865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ‘𝑖) ∈ V
70		dmeq 5868	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (ℎ‘𝑖) → dom 𝑠 = dom (ℎ‘𝑖))
71	70	eleq2d 2838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (ℎ‘𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘𝑖)))
72	70	eleq1d 2837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (ℎ‘𝑖) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘𝑖) ∈ ω))
73	71, 72	anbi12d 640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (ℎ‘𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω)))
74	69, 73	elab 3629	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))
75	68, 74	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))
76	75	simprd 498	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → dom (ℎ‘𝑖) ∈ ω)
77		nnord 7839	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (ℎ‘𝑖) ∈ ω → Ord dom (ℎ‘𝑖))
78		ordsucelsuc 7787	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord dom (ℎ‘𝑖) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
79	76, 77, 78	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
80	79	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
81		dmeq 5868	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (ℎ‘𝑖) → dom 𝑥 = dom (ℎ‘𝑖))
82		suceq 6399	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑥 = dom (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖))
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖))
84	83	eqeq2d 2763	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (ℎ‘𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (ℎ‘𝑖)))
85	81	reseq2d 5954	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (ℎ‘𝑖)))
86		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → 𝑥 = (ℎ‘𝑖))
87	85, 86	eqeq12d 2768	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (ℎ‘𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
88	84, 87	anbi12d 640	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (ℎ‘𝑖) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
89	88	rabbidv 3411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (ℎ‘𝑖) → {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)} = {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))})
90		axdc3lem2.3	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
91		axdc3lem2.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐴 ∈ V
92	91, 28	axdc3lem 10393	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑆 ∈ V
93	92	rabex 5285	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ∈ V
94	89, 90, 93	fvmpt 6960	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝐺‘(ℎ‘𝑖)) = {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))})
95	94	eleq2d 2838	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))}))
96		dmeq 5868	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (ℎ‘suc 𝑖) → dom 𝑦 = dom (ℎ‘suc 𝑖))
97	96	eqeq1d 2754	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (ℎ‘suc 𝑖) → (dom 𝑦 = suc dom (ℎ‘𝑖) ↔ dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖)))
98		reseq1 5948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (ℎ‘suc 𝑖) → (𝑦 ↾ dom (ℎ‘𝑖)) = ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)))
99	98	eqeq1d 2754	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (ℎ‘suc 𝑖) → ((𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) ↔ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
100	97, 99	anbi12d 640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (ℎ‘suc 𝑖) → ((dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)) ↔ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
101	100	elrab 3641	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
102	95, 101	bitrdi 289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))))
103	102	simplbda 502	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
104	103	simpld 497	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖))
105	104	eleq2d 2838	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
106	80, 105	bitr4d 284	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
107	106	biimpd 231	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) → suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
108	103	simprd 498	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))
109		resss 5976	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖)
110		sseq1 3952	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)))
111	109, 110	mpbii 235	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖))
112		elsuci 6400	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ suc 𝑖 → (𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖))
113		pm2.27 42	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))
114		sstr2 3934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑗) ⊆ (ℎ‘𝑖) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
115	113, 114	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
116		fveq2 6852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑖 → (ℎ‘𝑗) = (ℎ‘𝑖))
117	116	sseq1d 3958	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)))
118	117	biimprd 250	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
119	118	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
120	115, 119	jaoi 866	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖) → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
121	112, 120	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ suc 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
122	121	com13 88	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
123	108, 111, 122	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
124	107, 123	anim12d 617	. . . . . . . . . . . . 13 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
125	61, 67, 124	syl2anc 592	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
126	125	ex 415	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))))
127	8, 16, 24, 58, 126	finds2 7864	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))))
128	127	imp 409	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))
129	128	simprd 498	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))
130	129	expcom 416	. . . . . . 7 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))
131	130	ralrimdv 3150	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))
132	131	ralrimiv 3143	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚))
133		frn 6684	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ 𝑆)
134		ffun 6679	. . . . . . . . . . . . . . . 16 ⊢ (𝑠:suc 𝑛⟶𝐴 → Fun 𝑠)
135	134	3ad2ant1 1142	. . . . . . . . . . . . . . 15 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠)
136	135	rexlimivw 3149	. . . . . . . . . . . . . 14 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠)
137	136	ss2abi 4010	. . . . . . . . . . . . 13 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠}
138	28, 137	eqsstri 3973	. . . . . . . . . . . 12 ⊢ 𝑆 ⊆ {𝑠 ∣ Fun 𝑠}
139	133, 138	sstrdi 3939	. . . . . . . . . . 11 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ Fun 𝑠})
140	139	sseld 3926	. . . . . . . . . 10 ⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → 𝑢 ∈ {𝑠 ∣ Fun 𝑠}))
141		vex 3448	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
142		funeq 6526	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢))
143	141, 142	elab 3629	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢)
144	140, 143	imbitrdi 253	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → Fun 𝑢))
145	144	adantr 483	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → Fun 𝑢))
146		ffn 6676	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → ℎ Fn ω)
147		fvelrnb 6912	. . . . . . . . . . . . 13 ⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ ↔ ∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣))
148		fvelrnb 6912	. . . . . . . . . . . . . . 15 ⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ ↔ ∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢))
149		nnord 7839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ ω → Ord 𝑎)
150		nnord 7839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ ω → Ord 𝑏)
151	149, 150	anim12i 621	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord 𝑎 ∧ Ord 𝑏))
152		ordtri3or 6363	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎))
153		fveq2 6852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑏 → (ℎ‘𝑚) = (ℎ‘𝑏))
154	153	sseq2d 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
155	154	raleqbi1dv 3320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑏 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
156	155	rspcv 3568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
157		fveq2 6852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑎 → (ℎ‘𝑗) = (ℎ‘𝑎))
158	157	sseq1d 3958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑏) ↔ (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))
159	158	rspccv 3569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))
160	156, 159	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))))
161	160	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))))
162	161	3imp 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))
163	162	orcd 882	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
164	163	3exp 1128	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
165	164	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
166		fveq2 6852	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (ℎ‘𝑎) = (ℎ‘𝑏))
167		eqimss 3985	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))
168	167	orcd 882	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
169	166, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
170	169	2a1d 26	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
171		fveq2 6852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑎 → (ℎ‘𝑚) = (ℎ‘𝑎))
172	171	sseq2d 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
173	172	raleqbi1dv 3320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑎 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
174	173	rspcv 3568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
175		fveq2 6852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑏 → (ℎ‘𝑗) = (ℎ‘𝑏))
176	175	sseq1d 3958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑎) ↔ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
177	176	rspccv 3569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
178	174, 177	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
179	178	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
180	179	3imp 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))
181	180	olcd 883	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
182	181	3exp 1128	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
183	182	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ 𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
184	165, 170, 183	3jaoi 1439	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
185	152, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord 𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
186	151, 185	mpcom 38	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
187		sseq12 3954	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ↔ 𝑢 ⊆ 𝑣))
188		sseq12 3954	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ‘𝑏) = 𝑣 ∧ (ℎ‘𝑎) = 𝑢) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢))
189	188	ancoms 461	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢))
190	187, 189	orbi12d 927	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) ↔ (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
191	190	biimpcd 251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
192	186, 191	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
193	192	com23 86	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
194	193	exp4b 433	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ω → (𝑏 ∈ ω → ((ℎ‘𝑎) = 𝑢 → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))))
195	194	com23 86	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ω → ((ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))))
196	195	rexlimiv 3146	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
197	196	rexlimdv 3151	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢 → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
198	148, 197	biimtrdi 255	. . . . . . . . . . . . . 14 ⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
199	198	com23 86	. . . . . . . . . . . . 13 ⊢ (ℎ Fn ω → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
200	147, 199	sylbid 242	. . . . . . . . . . . 12 ⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
201	200	com24 95	. . . . . . . . . . 11 ⊢ (ℎ Fn ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
202	201	imp 409	. . . . . . . . . 10 ⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
203	202	ralrimdv 3150	. . . . . . . . 9 ⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
204	146, 203	sylan 588	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
205	145, 204	jcad 519	. . . . . . 7 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
206	205	ralrimiv 3143	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → ∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
207		fununi 6581	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → Fun ∪ ran ℎ)
208	206, 207	syl 17	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → Fun ∪ ran ℎ)
209	132, 208	syldan 599	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → Fun ∪ ran ℎ)
210		vex 3448	. . . . . . . . 9 ⊢ 𝑚 ∈ V
211	210	eldm2 5866	. . . . . . . 8 ⊢ (𝑚 ∈ dom ∪ ran ℎ ↔ ∃𝑢⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ)
212		eluni2 4859	. . . . . . . . . 10 ⊢ (⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ ↔ ∃𝑣 ∈ ran ℎ⟨𝑚, 𝑢⟩ ∈ 𝑣)
213	210, 141	opeldm 5872	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣)
214	213	a1i 11	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣))
215	133, 44	sstrdi 3939	. . . . . . . . . . . . . . 15 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
216		ssel 3921	. . . . . . . . . . . . . . . 16 ⊢ (ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran ℎ → 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
217		vex 3448	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑣 ∈ V
218		dmeq 5868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣)
219	218	eleq2d 2838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣))
220	218	eleq1d 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω))
221	219, 220	anbi12d 640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
222	217, 221	elab 3629	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))
223	222	simprbi 500	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → dom 𝑣 ∈ ω)
224	216, 223	syl6 35	. . . . . . . . . . . . . . 15 ⊢ (ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran ℎ → dom 𝑣 ∈ ω))
225	215, 224	syl 17	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (𝑣 ∈ ran ℎ → dom 𝑣 ∈ ω))
226	214, 225	anim12d 617	. . . . . . . . . . . . 13 ⊢ (ℎ:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
227		elnn 7842	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω)
228	226, 227	syl6 35	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → 𝑚 ∈ ω))
229	228	expcomd 419	. . . . . . . . . . 11 ⊢ (ℎ:ω⟶𝑆 → (𝑣 ∈ ran ℎ → (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ ω)))
230	229	rexlimdv 3151	. . . . . . . . . 10 ⊢ (ℎ:ω⟶𝑆 → (∃𝑣 ∈ ran ℎ⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ ω))
231	212, 230	biimtrid 244	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω))
232	231	exlimdv 1943	. . . . . . . 8 ⊢ (ℎ:ω⟶𝑆 → (∃𝑢⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω))
233	211, 232	biimtrid 244	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → (𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω))
234	233	adantr 483	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω))
235		id 22	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ω → 𝑚 ∈ ω)
236		fnfvelrn 7046	. . . . . . . . . . 11 ⊢ ((ℎ Fn ω ∧ 𝑚 ∈ ω) → (ℎ‘𝑚) ∈ ran ℎ)
237	146, 235, 236	syl2anr 605	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑚) ∈ ran ℎ)
238	237	adantrr 725	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑚) ∈ ran ℎ)
239	128	simpld 497	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom (ℎ‘𝑚))
240		dmeq 5868	. . . . . . . . . 10 ⊢ (𝑢 = (ℎ‘𝑚) → dom 𝑢 = dom (ℎ‘𝑚))
241	240	eliuni 4945	. . . . . . . . 9 ⊢ (((ℎ‘𝑚) ∈ ran ℎ ∧ 𝑚 ∈ dom (ℎ‘𝑚)) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎdom 𝑢)
242	238, 239, 241	syl2anc 592	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎdom 𝑢)
243		dmuni 5879	. . . . . . . 8 ⊢ dom ∪ ran ℎ = ∪ 𝑢 ∈ ran ℎdom 𝑢
244	242, 243	eleqtrrdi 2863	. . . . . . 7 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom ∪ ran ℎ)
245	244	expcom 416	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ∪ ran ℎ))
246	234, 245	impbid 214	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran ℎ ↔ 𝑚 ∈ ω))
247	246	eqrdv 2750	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → dom ∪ ran ℎ = ω)
248		rnuni 6119	. . . . . 6 ⊢ ran ∪ ran ℎ = ∪ 𝑠 ∈ ran ℎran 𝑠
249		frn 6684	. . . . . . . . . . . . . 14 ⊢ (𝑠:suc 𝑛⟶𝐴 → ran 𝑠 ⊆ 𝐴)
250	249	3ad2ant1 1142	. . . . . . . . . . . . 13 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴)
251	250	rexlimivw 3149	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴)
252	251	ss2abi 4010	. . . . . . . . . . 11 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}
253	28, 252	eqsstri 3973	. . . . . . . . . 10 ⊢ 𝑆 ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}
254	133, 253	sstrdi 3939	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴})
255		ssel 3921	. . . . . . . . . 10 ⊢ (ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → 𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}))
256		abid 2734	. . . . . . . . . 10 ⊢ (𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} ↔ ran 𝑠 ⊆ 𝐴)
257	255, 256	imbitrdi 253	. . . . . . . . 9 ⊢ (ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴))
258	254, 257	syl 17	. . . . . . . 8 ⊢ (ℎ:ω⟶𝑆 → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴))
259	258	ralrimiv 3143	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
260		iunss 4992	. . . . . . 7 ⊢ (∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴 ↔ ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
261	259, 260	sylibr 236	. . . . . 6 ⊢ (ℎ:ω⟶𝑆 → ∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
262	248, 261	eqsstrid 3965	. . . . 5 ⊢ (ℎ:ω⟶𝑆 → ran ∪ ran ℎ ⊆ 𝐴)
263	262	adantr 483	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ran ∪ ran ℎ ⊆ 𝐴)
264		df-fn 6509	. . . . 5 ⊢ (∪ ran ℎ Fn ω ↔ (Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω))
265		df-f 6510	. . . . . 6 ⊢ (∪ ran ℎ:ω⟶𝐴 ↔ (∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴))
266	265	biimpri 230	. . . . 5 ⊢ ((∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴)
267	264, 266	sylanbr 590	. . . 4 ⊢ (((Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω) ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴)
268	209, 247, 263, 267	syl21anc 846	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∪ ran ℎ:ω⟶𝐴)
269		fnfvelrn 7046	. . . . . . . 8 ⊢ ((ℎ Fn ω ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ ran ℎ)
270	146, 25, 269	sylancl 594	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ ran ℎ)
271	270	adantr 483	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ∈ ran ℎ)
272		elssuni 4887	. . . . . 6 ⊢ ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ⊆ ∪ ran ℎ)
273	271, 272	syl 17	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ⊆ ∪ ran ℎ)
274	54	adantr 483	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∅ ∈ dom (ℎ‘∅))
275		funssfv 6873	. . . . 5 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘∅) ⊆ ∪ ran ℎ ∧ ∅ ∈ dom (ℎ‘∅)) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅))
276	209, 273, 274, 275	syl3anc 1382	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅))
277		simp2 1146	. . . . . . . . . . 11 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶)
278	277	rexlimivw 3149	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶)
279	278	ss2abi 4010	. . . . . . . . 9 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
280	28, 279	eqsstri 3973	. . . . . . . 8 ⊢ 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
281	133, 280	sstrdi 3939	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶})
282		ssel 3921	. . . . . . . 8 ⊢ (ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶}))
283		fveq1 6851	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘∅) → (𝑠‘∅) = ((ℎ‘∅)‘∅))
284	283	eqeq1d 2754	. . . . . . . . 9 ⊢ (𝑠 = (ℎ‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((ℎ‘∅)‘∅) = 𝐶))
285	46, 284	elab 3629	. . . . . . . 8 ⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((ℎ‘∅)‘∅) = 𝐶)
286	282, 285	imbitrdi 253	. . . . . . 7 ⊢ (ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
287	281, 286	syl 17	. . . . . 6 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
288	287	adantr 483	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
289	271, 288	mpd 15	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅)‘∅) = 𝐶)
290	276, 289	eqtrd 2787	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran ℎ‘∅) = 𝐶)
291		nfv 1924	. . . . 5 ⊢ Ⅎ𝑘 ℎ:ω⟶𝑆
292		nfra1 3276	. . . . 5 ⊢ Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))
293	291, 292	nfan 1909	. . . 4 ⊢ Ⅎ𝑘(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
294	133	ad2antrr 734	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ran ℎ ⊆ 𝑆)
295		peano2 7855	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
296		fnfvelrn 7046	. . . . . . . . 9 ⊢ ((ℎ Fn ω ∧ suc 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
297	146, 295, 296	syl2an 604	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
298	297	adantlr 723	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
299	239	expcom 416	. . . . . . . . 9 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (ℎ‘𝑚)))
300	299	ralrimiv 3143	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚))
301		id 22	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑘 → 𝑚 = suc 𝑘)
302		fveq2 6852	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑘 → (ℎ‘𝑚) = (ℎ‘suc 𝑘))
303	302	dmeqd 5870	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑘 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑘))
304	301, 303	eleq12d 2846	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑘 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
305	304	rspcv 3568	. . . . . . . . 9 ⊢ (suc 𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
306	295, 305	syl 17	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
307	300, 306	mpan9 513	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘))
308		eleq2 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (dom 𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛))
309	308	biimpa 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
310	29, 309	sylan 588	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
311		ordsucelsuc 7787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑛 → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
312	30, 311	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ω → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
313	312	biimprd 250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛 → 𝑘 ∈ 𝑛))
314		rsp 3240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑘 ∈ 𝑛 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
315	313, 314	syl9r 78	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
316	315	com13 88	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑘 ∈ suc 𝑛 → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
317	310, 316	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
318	317	ex 415	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠:suc 𝑛⟶𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))))
319	318	com24 95	. . . . . . . . . . . . . . . 16 ⊢ (𝑠:suc 𝑛⟶𝐴 → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))))
320	319	imp 409	. . . . . . . . . . . . . . 15 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
321	320	3adant2 1140	. . . . . . . . . . . . . 14 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
322	321	impcom 410	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
323	322	rexlimiva 3145	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
324	323	ss2abi 4010	. . . . . . . . . . 11 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
325	28, 324	eqsstri 3973	. . . . . . . . . 10 ⊢ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
326		sstr 3935	. . . . . . . . . 10 ⊢ ((ran ℎ ⊆ 𝑆 ∧ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})
327	325, 326	mpan2 699	. . . . . . . . 9 ⊢ (ran ℎ ⊆ 𝑆 → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})
328	327	sseld 3926	. . . . . . . 8 ⊢ (ran ℎ ⊆ 𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}))
329		fvex 6865	. . . . . . . . 9 ⊢ (ℎ‘suc 𝑘) ∈ V
330		dmeq 5868	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → dom 𝑠 = dom (ℎ‘suc 𝑘))
331	330	eleq2d 2838	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
332		fveq1 6851	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
333		fveq1 6851	. . . . . . . . . . . 12 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
334	333	fveq2d 6856	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝐹‘(𝑠‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
335	332, 334	eleq12d 2846	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
336	331, 335	imbi12d 346	. . . . . . . . 9 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))))
337	329, 336	elab 3629	. . . . . . . 8 ⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
338	328, 337	imbitrdi 253	. . . . . . 7 ⊢ (ran ℎ ⊆ 𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))))
339	294, 298, 307, 338	syl3c 66	. . . . . 6 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
340	209	adantr 483	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → Fun ∪ ran ℎ)
341		elssuni 4887	. . . . . . . . . 10 ⊢ ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
342	297, 341	syl 17	. . . . . . . . 9 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
343	342	adantlr 723	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
344		funssfv 6873	. . . . . . . 8 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
345	340, 343, 307, 344	syl3anc 1382	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
346	215	sseld 3926	. . . . . . . . . . . . . . 15 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
347	330	eleq2d 2838	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘suc 𝑘)))
348	330	eleq1d 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘suc 𝑘) ∈ ω))
349	347, 348	anbi12d 640	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
350	329, 349	elab 3629	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))
351	346, 350	imbitrdi 253	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
352	351	adantr 483	. . . . . . . . . . . . 13 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
353	297, 352	mpd 15	. . . . . . . . . . . 12 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))
354	353	simprd 498	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → dom (ℎ‘suc 𝑘) ∈ ω)
355		nnord 7839	. . . . . . . . . . 11 ⊢ (dom (ℎ‘suc 𝑘) ∈ ω → Ord dom (ℎ‘suc 𝑘))
356		ordtr 6345	. . . . . . . . . . 11 ⊢ (Ord dom (ℎ‘suc 𝑘) → Tr dom (ℎ‘suc 𝑘))
357		trsuc 6420	. . . . . . . . . . . 12 ⊢ ((Tr dom (ℎ‘suc 𝑘) ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → 𝑘 ∈ dom (ℎ‘suc 𝑘))
358	357	ex 415	. . . . . . . . . . 11 ⊢ (Tr dom (ℎ‘suc 𝑘) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘)))
359	354, 355, 356, 358	4syl 19	. . . . . . . . . 10 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘)))
360	359	adantlr 723	. . . . . . . . 9 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘)))
361	307, 360	mpd 15	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom (ℎ‘suc 𝑘))
362		funssfv 6873	. . . . . . . 8 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ ∧ 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
363	340, 343, 361, 362	syl3anc 1382	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
364		simpl 485	. . . . . . . 8 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
365		simpr 487	. . . . . . . . 9 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
366	365	fveq2d 6856	. . . . . . . 8 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (𝐹‘(∪ ran ℎ‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
367	364, 366	eleq12d 2846	. . . . . . 7 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
368	345, 363, 367	syl2anc 592	. . . . . 6 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
369	339, 368	mpbird 259	. . . . 5 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))
370	369	ex 415	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑘 ∈ ω → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
371	293, 370	ralrimi 3250	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))
372		vex 3448	. . . . . 6 ⊢ ℎ ∈ V
373	372	rnex 7876	. . . . 5 ⊢ ran ℎ ∈ V
374	373	uniex 7709	. . . 4 ⊢ ∪ ran ℎ ∈ V
375		feq1 6654	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → (𝑔:ω⟶𝐴 ↔ ∪ ran ℎ:ω⟶𝐴))
376		fveq1 6851	. . . . . 6 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘∅) = (∪ ran ℎ‘∅))
377	376	eqeq1d 2754	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔‘∅) = 𝐶 ↔ (∪ ran ℎ‘∅) = 𝐶))
378		fveq1 6851	. . . . . . 7 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘suc 𝑘) = (∪ ran ℎ‘suc 𝑘))
379		fveq1 6851	. . . . . . . 8 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘𝑘) = (∪ ran ℎ‘𝑘))
380	379	fveq2d 6856	. . . . . . 7 ⊢ (𝑔 = ∪ ran ℎ → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(∪ ran ℎ‘𝑘)))
381	378, 380	eleq12d 2846	. . . . . 6 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
382	381	ralbidv 3175	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
383	375, 377, 382	3anbi123d 1447	. . . 4 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))))
384	374, 383	spcev 3556	. . 3 ⊢ ((∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
385	268, 290, 371, 384	syl3anc 1382	. 2 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
386	385	exlimiv 1940	1 ⊢ (∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 856   ∨ w3o 1094   ∧ w3a 1095   = wceq 1550  ∃wex 1789   ∈ wcel 2132  {cab 2730  ∀wral 3066  ∃wrex 3076  {crab 3404  Vcvv 3444   ⊆ wss 3895  ∅c0 4276  ⟨cop 4578  ∪ cuni 4855  ∪ ciun 4939   ↦ cmpt 5171  Tr wtr 5197  dom cdm 5636  ran crn 5637   ↾ cres 5638  Ord word 6330  suc csuc 6333  Fun wfun 6500   Fn wfn 6501  ⟶wf 6502  ‘cfv 6506  ωcom 7831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-dc 10389

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-pss 3915  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-iun 4941  df-br 5091  df-opab 5153  df-mpt 5172  df-tr 5198  df-id 5531  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5589  df-we 5591  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ord 6334  df-on 6335  df-lim 6336  df-suc 6337  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-fv 6514  df-om 7832  df-1o 8421

This theorem is referenced by:  axdc3lem4  10396