Theorem axdc3lem2 10476

Description: Lemma for axdc3 10479. 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 10471 (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 10471 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 6896	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅))
3	2	dmeqd 5908	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → dom (ℎ‘𝑚) = dom (ℎ‘∅))
4	1, 3	eleq12d 2819	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑚 ∈ dom (ℎ‘𝑚) ↔ ∅ ∈ dom (ℎ‘∅)))
5		eleq2 2814	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ ∅))
6	2	sseq2d 4009	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘∅)))
7	5, 6	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
8	4, 7	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))))
9		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → 𝑚 = 𝑖)
10		fveq2 6896	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖))
11	10	dmeqd 5908	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘𝑖))
12	9, 11	eleq12d 2819	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ 𝑖 ∈ dom (ℎ‘𝑖)))
13		elequ2 2113	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ 𝑖))
14	10	sseq2d 4009	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))
15	13, 14	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))))
16	12, 15	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))))
17		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → 𝑚 = suc 𝑖)
18		fveq2 6896	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖))
19	18	dmeqd 5908	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑖))
20	17, 19	eleq12d 2819	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
21		eleq2 2814	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ suc 𝑖))
22	18	sseq2d 4009	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
23	21, 22	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
24	20, 23	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
25		peano1 7895	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
26		ffvelcdm 7090	. . . . . . . . . . . . . . 15 ⊢ ((ℎ:ω⟶𝑆 ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ 𝑆)
27	25, 26	mpan2 689	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ 𝑆)
28		axdc3lem2.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
29		fdm 6732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠:suc 𝑛⟶𝐴 → dom 𝑠 = suc 𝑛)
30		nnord 7879	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ω → Ord 𝑛)
31		0elsuc 7839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑛 → ∅ ∈ suc 𝑛)
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → ∅ ∈ suc 𝑛)
33		peano2 7897	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
34		eleq2 2814	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛))
35		eleq1 2813	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω))
36	34, 35	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (dom 𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω)))
37	36	biimprcd 249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
38	32, 33, 37	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
39	29, 38	syl5com 31	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠:suc 𝑛⟶𝐴 → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
40	39	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
41	40	impcom 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
42	41	rexlimiva 3136	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
43	42	ss2abi 4059	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
44	28, 43	eqsstri 4011	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
45	44	sseli 3972	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘∅) ∈ 𝑆 → (ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
46		fvex 6909	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ‘∅) ∈ V
47		dmeq 5906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = (ℎ‘∅) → dom 𝑠 = dom (ℎ‘∅))
48	47	eleq2d 2811	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (ℎ‘∅) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘∅)))
49	47	eleq1d 2810	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (ℎ‘∅) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘∅) ∈ ω))
50	48, 49	anbi12d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘∅) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω)))
51	46, 50	elab 3664	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω))
52	45, 51	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘∅) ∈ 𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω))
53	52	simpld 493	. . . . . . . . . . . . . 14 ⊢ ((ℎ‘∅) ∈ 𝑆 → ∅ ∈ dom (ℎ‘∅))
54	27, 53	syl 17	. . . . . . . . . . . . 13 ⊢ (ℎ:ω⟶𝑆 → ∅ ∈ dom (ℎ‘∅))
55		noel 4330	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑗 ∈ ∅
56	55	pm2.21i 119	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))
57	54, 56	jctir 519	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
58	57	adantr 479	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
59		ffvelcdm 7090	. . . . . . . . . . . . . . 15 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ 𝑆)
60	59	ancoms 457	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑖) ∈ 𝑆)
61	60	adantrr 715	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑖) ∈ 𝑆)
62		suceq 6437	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
63	62	fveq2d 6900	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
64		2fveq3 6901	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖)))
65	63, 64	eleq12d 2819	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
66	65	rspcva 3604	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))
67	66	adantrl 714	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))
68	44	sseli 3972	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
69		fvex 6909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ‘𝑖) ∈ V
70		dmeq 5906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (ℎ‘𝑖) → dom 𝑠 = dom (ℎ‘𝑖))
71	70	eleq2d 2811	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (ℎ‘𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘𝑖)))
72	70	eleq1d 2810	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (ℎ‘𝑖) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘𝑖) ∈ ω))
73	71, 72	anbi12d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (ℎ‘𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω)))
74	69, 73	elab 3664	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))
75	68, 74	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))
76	75	simprd 494	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → dom (ℎ‘𝑖) ∈ ω)
77		nnord 7879	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (ℎ‘𝑖) ∈ ω → Ord dom (ℎ‘𝑖))
78		ordsucelsuc 7826	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord dom (ℎ‘𝑖) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
79	76, 77, 78	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
80	79	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
81		dmeq 5906	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (ℎ‘𝑖) → dom 𝑥 = dom (ℎ‘𝑖))
82		suceq 6437	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑥 = dom (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖))
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖))
84	83	eqeq2d 2736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (ℎ‘𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (ℎ‘𝑖)))
85	81	reseq2d 5985	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (ℎ‘𝑖)))
86		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → 𝑥 = (ℎ‘𝑖))
87	85, 86	eqeq12d 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (ℎ‘𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
88	84, 87	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (ℎ‘𝑖) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
89	88	rabbidv 3426	. . . . . . . . . . . . . . . . . . . . . 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 10475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑆 ∈ V
93	92	rabex 5335	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ∈ V
94	89, 90, 93	fvmpt 7004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝐺‘(ℎ‘𝑖)) = {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))})
95	94	eleq2d 2811	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))}))
96		dmeq 5906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (ℎ‘suc 𝑖) → dom 𝑦 = dom (ℎ‘suc 𝑖))
97	96	eqeq1d 2727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (ℎ‘suc 𝑖) → (dom 𝑦 = suc dom (ℎ‘𝑖) ↔ dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖)))
98		reseq1 5979	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (ℎ‘suc 𝑖) → (𝑦 ↾ dom (ℎ‘𝑖)) = ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)))
99	98	eqeq1d 2727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (ℎ‘suc 𝑖) → ((𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) ↔ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
100	97, 99	anbi12d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (ℎ‘suc 𝑖) → ((dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)) ↔ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
101	100	elrab 3679	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
102	95, 101	bitrdi 286	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))))
103	102	simplbda 498	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
104	103	simpld 493	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖))
105	104	eleq2d 2811	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
106	80, 105	bitr4d 281	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
107	106	biimpd 228	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) → suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
108	103	simprd 494	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))
109		resss 6007	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖)
110		sseq1 4002	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)))
111	109, 110	mpbii 232	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖))
112		elsuci 6438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ suc 𝑖 → (𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖))
113		pm2.27 42	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))
114		sstr2 3983	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑗) ⊆ (ℎ‘𝑖) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
115	113, 114	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
116		fveq2 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑖 → (ℎ‘𝑗) = (ℎ‘𝑖))
117	116	sseq1d 4008	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)))
118	117	biimprd 247	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
119	118	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
120	115, 119	jaoi 855	. . . . . . . . . . . . . . . . 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 607	. . . . . . . . . . . . 13 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
125	61, 67, 124	syl2anc 582	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
126	125	ex 411	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))))
127	8, 16, 24, 58, 126	finds2 7906	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))))
128	127	imp 405	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))
129	128	simprd 494	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))
130	129	expcom 412	. . . . . . 7 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))
131	130	ralrimdv 3141	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))
132	131	ralrimiv 3134	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚))
133		frn 6730	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ 𝑆)
134		ffun 6726	. . . . . . . . . . . . . . . 16 ⊢ (𝑠:suc 𝑛⟶𝐴 → Fun 𝑠)
135	134	3ad2ant1 1130	. . . . . . . . . . . . . . 15 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠)
136	135	rexlimivw 3140	. . . . . . . . . . . . . 14 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠)
137	136	ss2abi 4059	. . . . . . . . . . . . 13 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠}
138	28, 137	eqsstri 4011	. . . . . . . . . . . 12 ⊢ 𝑆 ⊆ {𝑠 ∣ Fun 𝑠}
139	133, 138	sstrdi 3989	. . . . . . . . . . 11 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ Fun 𝑠})
140	139	sseld 3975	. . . . . . . . . 10 ⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → 𝑢 ∈ {𝑠 ∣ Fun 𝑠}))
141		vex 3465	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
142		funeq 6574	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢))
143	141, 142	elab 3664	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢)
144	140, 143	imbitrdi 250	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → Fun 𝑢))
145	144	adantr 479	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → Fun 𝑢))
146		ffn 6723	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → ℎ Fn ω)
147		fvelrnb 6958	. . . . . . . . . . . . 13 ⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ ↔ ∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣))
148		fvelrnb 6958	. . . . . . . . . . . . . . 15 ⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ ↔ ∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢))
149		nnord 7879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ ω → Ord 𝑎)
150		nnord 7879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ ω → Ord 𝑏)
151	149, 150	anim12i 611	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord 𝑎 ∧ Ord 𝑏))
152		ordtri3or 6403	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎))
153		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑏 → (ℎ‘𝑚) = (ℎ‘𝑏))
154	153	sseq2d 4009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
155	154	raleqbi1dv 3322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑏 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
156	155	rspcv 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
157		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑎 → (ℎ‘𝑗) = (ℎ‘𝑎))
158	157	sseq1d 4008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑏) ↔ (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))
159	158	rspccv 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))
160	156, 159	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))))
161	160	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))))
162	161	3imp 1108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))
163	162	orcd 871	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
164	163	3exp 1116	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
165	164	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
166		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (ℎ‘𝑎) = (ℎ‘𝑏))
167		eqimss 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))
168	167	orcd 871	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
169	166, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
170	169	2a1d 26	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
171		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑎 → (ℎ‘𝑚) = (ℎ‘𝑎))
172	171	sseq2d 4009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
173	172	raleqbi1dv 3322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑎 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
174	173	rspcv 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
175		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑏 → (ℎ‘𝑗) = (ℎ‘𝑏))
176	175	sseq1d 4008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑎) ↔ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
177	176	rspccv 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
178	174, 177	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
179	178	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
180	179	3imp 1108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))
181	180	olcd 872	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
182	181	3exp 1116	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
183	182	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ 𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
184	165, 170, 183	3jaoi 1424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
185	152, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord 𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
186	151, 185	mpcom 38	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
187		sseq12 4004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ↔ 𝑢 ⊆ 𝑣))
188		sseq12 4004	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ‘𝑏) = 𝑣 ∧ (ℎ‘𝑎) = 𝑢) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢))
189	188	ancoms 457	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢))
190	187, 189	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) ↔ (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
191	190	biimpcd 248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
192	186, 191	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
193	192	com23 86	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
194	193	exp4b 429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ω → (𝑏 ∈ ω → ((ℎ‘𝑎) = 𝑢 → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))))
195	194	com23 86	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ω → ((ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))))
196	195	rexlimiv 3137	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
197	196	rexlimdv 3142	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢 → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
198	148, 197	biimtrdi 252	. . . . . . . . . . . . . 14 ⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
199	198	com23 86	. . . . . . . . . . . . 13 ⊢ (ℎ Fn ω → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
200	147, 199	sylbid 239	. . . . . . . . . . . 12 ⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
201	200	com24 95	. . . . . . . . . . 11 ⊢ (ℎ Fn ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
202	201	imp 405	. . . . . . . . . 10 ⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
203	202	ralrimdv 3141	. . . . . . . . 9 ⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
204	146, 203	sylan 578	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
205	145, 204	jcad 511	. . . . . . 7 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
206	205	ralrimiv 3134	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → ∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
207		fununi 6629	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → Fun ∪ ran ℎ)
208	206, 207	syl 17	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → Fun ∪ ran ℎ)
209	132, 208	syldan 589	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → Fun ∪ ran ℎ)
210		vex 3465	. . . . . . . . 9 ⊢ 𝑚 ∈ V
211	210	eldm2 5904	. . . . . . . 8 ⊢ (𝑚 ∈ dom ∪ ran ℎ ↔ ∃𝑢⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ)
212		eluni2 4913	. . . . . . . . . 10 ⊢ (⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ ↔ ∃𝑣 ∈ ran ℎ⟨𝑚, 𝑢⟩ ∈ 𝑣)
213	210, 141	opeldm 5910	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣)
214	213	a1i 11	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣))
215	133, 44	sstrdi 3989	. . . . . . . . . . . . . . 15 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
216		ssel 3970	. . . . . . . . . . . . . . . 16 ⊢ (ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran ℎ → 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
217		vex 3465	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑣 ∈ V
218		dmeq 5906	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣)
219	218	eleq2d 2811	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣))
220	218	eleq1d 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω))
221	219, 220	anbi12d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
222	217, 221	elab 3664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))
223	222	simprbi 495	. . . . . . . . . . . . . . . 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 607	. . . . . . . . . . . . 13 ⊢ (ℎ:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
227		elnn 7882	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω)
228	226, 227	syl6 35	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → 𝑚 ∈ ω))
229	228	expcomd 415	. . . . . . . . . . 11 ⊢ (ℎ:ω⟶𝑆 → (𝑣 ∈ ran ℎ → (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ ω)))
230	229	rexlimdv 3142	. . . . . . . . . 10 ⊢ (ℎ:ω⟶𝑆 → (∃𝑣 ∈ ran ℎ⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ ω))
231	212, 230	biimtrid 241	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω))
232	231	exlimdv 1928	. . . . . . . 8 ⊢ (ℎ:ω⟶𝑆 → (∃𝑢⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω))
233	211, 232	biimtrid 241	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → (𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω))
234	233	adantr 479	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω))
235		id 22	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ω → 𝑚 ∈ ω)
236		fnfvelrn 7089	. . . . . . . . . . 11 ⊢ ((ℎ Fn ω ∧ 𝑚 ∈ ω) → (ℎ‘𝑚) ∈ ran ℎ)
237	146, 235, 236	syl2anr 595	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑚) ∈ ran ℎ)
238	237	adantrr 715	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑚) ∈ ran ℎ)
239	128	simpld 493	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom (ℎ‘𝑚))
240		dmeq 5906	. . . . . . . . . 10 ⊢ (𝑢 = (ℎ‘𝑚) → dom 𝑢 = dom (ℎ‘𝑚))
241	240	eliuni 5003	. . . . . . . . 9 ⊢ (((ℎ‘𝑚) ∈ ran ℎ ∧ 𝑚 ∈ dom (ℎ‘𝑚)) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎdom 𝑢)
242	238, 239, 241	syl2anc 582	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎdom 𝑢)
243		dmuni 5917	. . . . . . . 8 ⊢ dom ∪ ran ℎ = ∪ 𝑢 ∈ ran ℎdom 𝑢
244	242, 243	eleqtrrdi 2836	. . . . . . 7 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom ∪ ran ℎ)
245	244	expcom 412	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ∪ ran ℎ))
246	234, 245	impbid 211	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran ℎ ↔ 𝑚 ∈ ω))
247	246	eqrdv 2723	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → dom ∪ ran ℎ = ω)
248		rnuni 6155	. . . . . 6 ⊢ ran ∪ ran ℎ = ∪ 𝑠 ∈ ran ℎran 𝑠
249		frn 6730	. . . . . . . . . . . . . 14 ⊢ (𝑠:suc 𝑛⟶𝐴 → ran 𝑠 ⊆ 𝐴)
250	249	3ad2ant1 1130	. . . . . . . . . . . . 13 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴)
251	250	rexlimivw 3140	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴)
252	251	ss2abi 4059	. . . . . . . . . . 11 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}
253	28, 252	eqsstri 4011	. . . . . . . . . 10 ⊢ 𝑆 ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}
254	133, 253	sstrdi 3989	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴})
255		ssel 3970	. . . . . . . . . 10 ⊢ (ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → 𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}))
256		abid 2706	. . . . . . . . . 10 ⊢ (𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} ↔ ran 𝑠 ⊆ 𝐴)
257	255, 256	imbitrdi 250	. . . . . . . . 9 ⊢ (ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴))
258	254, 257	syl 17	. . . . . . . 8 ⊢ (ℎ:ω⟶𝑆 → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴))
259	258	ralrimiv 3134	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
260		iunss 5049	. . . . . . 7 ⊢ (∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴 ↔ ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
261	259, 260	sylibr 233	. . . . . 6 ⊢ (ℎ:ω⟶𝑆 → ∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
262	248, 261	eqsstrid 4025	. . . . 5 ⊢ (ℎ:ω⟶𝑆 → ran ∪ ran ℎ ⊆ 𝐴)
263	262	adantr 479	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ran ∪ ran ℎ ⊆ 𝐴)
264		df-fn 6552	. . . . 5 ⊢ (∪ ran ℎ Fn ω ↔ (Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω))
265		df-f 6553	. . . . . 6 ⊢ (∪ ran ℎ:ω⟶𝐴 ↔ (∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴))
266	265	biimpri 227	. . . . 5 ⊢ ((∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴)
267	264, 266	sylanbr 580	. . . 4 ⊢ (((Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω) ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴)
268	209, 247, 263, 267	syl21anc 836	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∪ ran ℎ:ω⟶𝐴)
269		fnfvelrn 7089	. . . . . . . 8 ⊢ ((ℎ Fn ω ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ ran ℎ)
270	146, 25, 269	sylancl 584	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ ran ℎ)
271	270	adantr 479	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ∈ ran ℎ)
272		elssuni 4941	. . . . . 6 ⊢ ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ⊆ ∪ ran ℎ)
273	271, 272	syl 17	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ⊆ ∪ ran ℎ)
274	54	adantr 479	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∅ ∈ dom (ℎ‘∅))
275		funssfv 6917	. . . . 5 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘∅) ⊆ ∪ ran ℎ ∧ ∅ ∈ dom (ℎ‘∅)) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅))
276	209, 273, 274, 275	syl3anc 1368	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅))
277		simp2 1134	. . . . . . . . . . 11 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶)
278	277	rexlimivw 3140	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶)
279	278	ss2abi 4059	. . . . . . . . 9 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
280	28, 279	eqsstri 4011	. . . . . . . 8 ⊢ 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
281	133, 280	sstrdi 3989	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶})
282		ssel 3970	. . . . . . . 8 ⊢ (ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶}))
283		fveq1 6895	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘∅) → (𝑠‘∅) = ((ℎ‘∅)‘∅))
284	283	eqeq1d 2727	. . . . . . . . 9 ⊢ (𝑠 = (ℎ‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((ℎ‘∅)‘∅) = 𝐶))
285	46, 284	elab 3664	. . . . . . . 8 ⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((ℎ‘∅)‘∅) = 𝐶)
286	282, 285	imbitrdi 250	. . . . . . 7 ⊢ (ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
287	281, 286	syl 17	. . . . . 6 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
288	287	adantr 479	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
289	271, 288	mpd 15	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅)‘∅) = 𝐶)
290	276, 289	eqtrd 2765	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran ℎ‘∅) = 𝐶)
291		nfv 1909	. . . . 5 ⊢ Ⅎ𝑘 ℎ:ω⟶𝑆
292		nfra1 3271	. . . . 5 ⊢ Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))
293	291, 292	nfan 1894	. . . 4 ⊢ Ⅎ𝑘(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
294	133	ad2antrr 724	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ran ℎ ⊆ 𝑆)
295		peano2 7897	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
296		fnfvelrn 7089	. . . . . . . . 9 ⊢ ((ℎ Fn ω ∧ suc 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
297	146, 295, 296	syl2an 594	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
298	297	adantlr 713	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
299	239	expcom 412	. . . . . . . . 9 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (ℎ‘𝑚)))
300	299	ralrimiv 3134	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚))
301		id 22	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑘 → 𝑚 = suc 𝑘)
302		fveq2 6896	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑘 → (ℎ‘𝑚) = (ℎ‘suc 𝑘))
303	302	dmeqd 5908	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑘 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑘))
304	301, 303	eleq12d 2819	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑘 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
305	304	rspcv 3602	. . . . . . . . 9 ⊢ (suc 𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
306	295, 305	syl 17	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
307	300, 306	mpan9 505	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘))
308		eleq2 2814	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (dom 𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛))
309	308	biimpa 475	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
310	29, 309	sylan 578	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
311		ordsucelsuc 7826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑛 → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
312	30, 311	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ω → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
313	312	biimprd 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛 → 𝑘 ∈ 𝑛))
314		rsp 3234	. . . . . . . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠:suc 𝑛⟶𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))))
319	318	com24 95	. . . . . . . . . . . . . . . 16 ⊢ (𝑠:suc 𝑛⟶𝐴 → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))))
320	319	imp 405	. . . . . . . . . . . . . . 15 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
321	320	3adant2 1128	. . . . . . . . . . . . . 14 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
322	321	impcom 406	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
323	322	rexlimiva 3136	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
324	323	ss2abi 4059	. . . . . . . . . . 11 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
325	28, 324	eqsstri 4011	. . . . . . . . . 10 ⊢ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
326		sstr 3985	. . . . . . . . . 10 ⊢ ((ran ℎ ⊆ 𝑆 ∧ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})
327	325, 326	mpan2 689	. . . . . . . . 9 ⊢ (ran ℎ ⊆ 𝑆 → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})
328	327	sseld 3975	. . . . . . . 8 ⊢ (ran ℎ ⊆ 𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}))
329		fvex 6909	. . . . . . . . 9 ⊢ (ℎ‘suc 𝑘) ∈ V
330		dmeq 5906	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → dom 𝑠 = dom (ℎ‘suc 𝑘))
331	330	eleq2d 2811	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
332		fveq1 6895	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
333		fveq1 6895	. . . . . . . . . . . 12 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
334	333	fveq2d 6900	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝐹‘(𝑠‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
335	332, 334	eleq12d 2819	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
336	331, 335	imbi12d 343	. . . . . . . . 9 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))))
337	329, 336	elab 3664	. . . . . . . 8 ⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
338	328, 337	imbitrdi 250	. . . . . . 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 479	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → Fun ∪ ran ℎ)
341		elssuni 4941	. . . . . . . . . 10 ⊢ ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
342	297, 341	syl 17	. . . . . . . . 9 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
343	342	adantlr 713	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
344		funssfv 6917	. . . . . . . 8 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
345	340, 343, 307, 344	syl3anc 1368	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
346	215	sseld 3975	. . . . . . . . . . . . . . 15 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
347	330	eleq2d 2811	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘suc 𝑘)))
348	330	eleq1d 2810	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘suc 𝑘) ∈ ω))
349	347, 348	anbi12d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
350	329, 349	elab 3664	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))
351	346, 350	imbitrdi 250	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
352	351	adantr 479	. . . . . . . . . . . . 13 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
353	297, 352	mpd 15	. . . . . . . . . . . 12 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))
354	353	simprd 494	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → dom (ℎ‘suc 𝑘) ∈ ω)
355		nnord 7879	. . . . . . . . . . 11 ⊢ (dom (ℎ‘suc 𝑘) ∈ ω → Ord dom (ℎ‘suc 𝑘))
356		ordtr 6385	. . . . . . . . . . 11 ⊢ (Ord dom (ℎ‘suc 𝑘) → Tr dom (ℎ‘suc 𝑘))
357		trsuc 6458	. . . . . . . . . . . 12 ⊢ ((Tr dom (ℎ‘suc 𝑘) ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → 𝑘 ∈ dom (ℎ‘suc 𝑘))
358	357	ex 411	. . . . . . . . . . 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 713	. . . . . . . . 9 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘)))
361	307, 360	mpd 15	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom (ℎ‘suc 𝑘))
362		funssfv 6917	. . . . . . . 8 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ ∧ 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
363	340, 343, 361, 362	syl3anc 1368	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
364		simpl 481	. . . . . . . 8 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
365		simpr 483	. . . . . . . . 9 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
366	365	fveq2d 6900	. . . . . . . 8 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (𝐹‘(∪ ran ℎ‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
367	364, 366	eleq12d 2819	. . . . . . 7 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
368	345, 363, 367	syl2anc 582	. . . . . 6 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
369	339, 368	mpbird 256	. . . . 5 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))
370	369	ex 411	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑘 ∈ ω → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
371	293, 370	ralrimi 3244	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))
372		vex 3465	. . . . . 6 ⊢ ℎ ∈ V
373	372	rnex 7918	. . . . 5 ⊢ ran ℎ ∈ V
374	373	uniex 7747	. . . 4 ⊢ ∪ ran ℎ ∈ V
375		feq1 6704	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → (𝑔:ω⟶𝐴 ↔ ∪ ran ℎ:ω⟶𝐴))
376		fveq1 6895	. . . . . 6 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘∅) = (∪ ran ℎ‘∅))
377	376	eqeq1d 2727	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔‘∅) = 𝐶 ↔ (∪ ran ℎ‘∅) = 𝐶))
378		fveq1 6895	. . . . . . 7 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘suc 𝑘) = (∪ ran ℎ‘suc 𝑘))
379		fveq1 6895	. . . . . . . 8 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘𝑘) = (∪ ran ℎ‘𝑘))
380	379	fveq2d 6900	. . . . . . 7 ⊢ (𝑔 = ∪ ran ℎ → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(∪ ran ℎ‘𝑘)))
381	378, 380	eleq12d 2819	. . . . . 6 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
382	381	ralbidv 3167	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
383	375, 377, 382	3anbi123d 1432	. . . 4 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))))
384	374, 383	spcev 3590	. . 3 ⊢ ((∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
385	268, 290, 371, 384	syl3anc 1368	. 2 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
386	385	exlimiv 1925	1 ⊢ (∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533  ∃wex 1773   ∈ wcel 2098  {cab 2702  ∀wral 3050  ∃wrex 3059  {crab 3418  Vcvv 3461   ⊆ wss 3944  ∅c0 4322  ⟨cop 4636  ∪ cuni 4909  ∪ ciun 4997   ↦ cmpt 5232  Tr wtr 5266  dom cdm 5678  ran crn 5679   ↾ cres 5680  Ord word 6370  suc csuc 6373  Fun wfun 6543   Fn wfn 6544  ⟶wf 6545  ‘cfv 6549  ωcom 7871

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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-dc 10471

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-fv 6557  df-om 7872  df-1o 8487

This theorem is referenced by:  axdc3lem4  10478