Theorem axdc3lem2 9558

Description: Lemma for axdc3 9561. 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 9553 (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 9553 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 6408	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅))
3	2	dmeqd 5527	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → dom (ℎ‘𝑚) = dom (ℎ‘∅))
4	1, 3	eleq12d 2879	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑚 ∈ dom (ℎ‘𝑚) ↔ ∅ ∈ dom (ℎ‘∅)))
5		eleq2 2874	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ ∅))
6	2	sseq2d 3830	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘∅)))
7	5, 6	imbi12d 335	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
8	4, 7	anbi12d 618	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))))
9		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → 𝑚 = 𝑖)
10		fveq2 6408	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖))
11	10	dmeqd 5527	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘𝑖))
12	9, 11	eleq12d 2879	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ 𝑖 ∈ dom (ℎ‘𝑖)))
13		elequ2 2170	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ 𝑖))
14	10	sseq2d 3830	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))
15	13, 14	imbi12d 335	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))))
16	12, 15	anbi12d 618	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))))
17		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → 𝑚 = suc 𝑖)
18		fveq2 6408	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖))
19	18	dmeqd 5527	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑖))
20	17, 19	eleq12d 2879	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
21		eleq2 2874	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ suc 𝑖))
22	18	sseq2d 3830	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
23	21, 22	imbi12d 335	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
24	20, 23	anbi12d 618	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
25		peano1 7315	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
26		ffvelrn 6579	. . . . . . . . . . . . . . 15 ⊢ ((ℎ:ω⟶𝑆 ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ 𝑆)
27	25, 26	mpan2 674	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ 𝑆)
28		axdc3lem2.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
29		fdm 6264	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠:suc 𝑛⟶𝐴 → dom 𝑠 = suc 𝑛)
30		nnord 7303	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ω → Ord 𝑛)
31		0elsuc 7265	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑛 → ∅ ∈ suc 𝑛)
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → ∅ ∈ suc 𝑛)
33		peano2 7316	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
34		eleq2 2874	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛))
35		eleq1 2873	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω))
36	34, 35	anbi12d 618	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (dom 𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω)))
37	36	biimprcd 241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
38	32, 33, 37	syl2anc 575	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
39	29, 38	syl5com 31	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠:suc 𝑛⟶𝐴 → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
40	39	3ad2ant1 1156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
41	40	impcom 396	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
42	41	rexlimiva 3216	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
43	42	ss2abi 3871	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
44	28, 43	eqsstri 3832	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
45	44	sseli 3794	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘∅) ∈ 𝑆 → (ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
46		fvex 6421	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ‘∅) ∈ V
47		dmeq 5525	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = (ℎ‘∅) → dom 𝑠 = dom (ℎ‘∅))
48	47	eleq2d 2871	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (ℎ‘∅) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘∅)))
49	47	eleq1d 2870	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (ℎ‘∅) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘∅) ∈ ω))
50	48, 49	anbi12d 618	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘∅) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω)))
51	46, 50	elab 3545	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω))
52	45, 51	sylib 209	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘∅) ∈ 𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω))
53	52	simpld 484	. . . . . . . . . . . . . 14 ⊢ ((ℎ‘∅) ∈ 𝑆 → ∅ ∈ dom (ℎ‘∅))
54	27, 53	syl 17	. . . . . . . . . . . . 13 ⊢ (ℎ:ω⟶𝑆 → ∅ ∈ dom (ℎ‘∅))
55		noel 4120	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑗 ∈ ∅
56	55	pm2.21i 117	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))
57	54, 56	jctir 512	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
58	57	adantr 468	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
59		ffvelrn 6579	. . . . . . . . . . . . . . 15 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ 𝑆)
60	59	ancoms 448	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑖) ∈ 𝑆)
61	60	adantrr 699	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑖) ∈ 𝑆)
62		suceq 6003	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
63	62	fveq2d 6412	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
64		2fveq3 6413	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖)))
65	63, 64	eleq12d 2879	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
66	65	rspcva 3500	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))
67	66	adantrl 698	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))
68	44	sseli 3794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
69		fvex 6421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ‘𝑖) ∈ V
70		dmeq 5525	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (ℎ‘𝑖) → dom 𝑠 = dom (ℎ‘𝑖))
71	70	eleq2d 2871	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (ℎ‘𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘𝑖)))
72	70	eleq1d 2870	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (ℎ‘𝑖) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘𝑖) ∈ ω))
73	71, 72	anbi12d 618	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (ℎ‘𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω)))
74	69, 73	elab 3545	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))
75	68, 74	sylib 209	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))
76	75	simprd 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → dom (ℎ‘𝑖) ∈ ω)
77		nnord 7303	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (ℎ‘𝑖) ∈ ω → Ord dom (ℎ‘𝑖))
78		ordsucelsuc 7252	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord dom (ℎ‘𝑖) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
79	76, 77, 78	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
80	79	adantr 468	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
81		dmeq 5525	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (ℎ‘𝑖) → dom 𝑥 = dom (ℎ‘𝑖))
82		suceq 6003	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑥 = dom (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖))
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖))
84	83	eqeq2d 2816	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (ℎ‘𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (ℎ‘𝑖)))
85	81	reseq2d 5597	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (ℎ‘𝑖)))
86		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → 𝑥 = (ℎ‘𝑖))
87	85, 86	eqeq12d 2821	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (ℎ‘𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
88	84, 87	anbi12d 618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (ℎ‘𝑖) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
89	88	rabbidv 3379	. . . . . . . . . . . . . . . . . . . . . 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 9557	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑆 ∈ V
93	92	rabex 5007	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ∈ V
94	89, 90, 93	fvmpt 6503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝐺‘(ℎ‘𝑖)) = {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))})
95	94	eleq2d 2871	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))}))
96		dmeq 5525	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (ℎ‘suc 𝑖) → dom 𝑦 = dom (ℎ‘suc 𝑖))
97	96	eqeq1d 2808	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (ℎ‘suc 𝑖) → (dom 𝑦 = suc dom (ℎ‘𝑖) ↔ dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖)))
98		reseq1 5591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (ℎ‘suc 𝑖) → (𝑦 ↾ dom (ℎ‘𝑖)) = ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)))
99	98	eqeq1d 2808	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (ℎ‘suc 𝑖) → ((𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) ↔ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
100	97, 99	anbi12d 618	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (ℎ‘suc 𝑖) → ((dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)) ↔ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
101	100	elrab 3559	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
102	95, 101	syl6bb 278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))))
103	102	simplbda 489	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
104	103	simpld 484	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖))
105	104	eleq2d 2871	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
106	80, 105	bitr4d 273	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
107	106	biimpd 220	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) → suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
108	103	simprd 485	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))
109		resss 5625	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖)
110		sseq1 3823	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)))
111	109, 110	mpbii 224	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖))
112		elsuci 6004	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ suc 𝑖 → (𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖))
113		pm2.27 42	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))
114		sstr2 3805	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑗) ⊆ (ℎ‘𝑖) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
115	113, 114	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
116		fveq2 6408	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑖 → (ℎ‘𝑗) = (ℎ‘𝑖))
117	116	sseq1d 3829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)))
118	117	biimprd 239	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
119	118	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
120	115, 119	jaoi 875	. . . . . . . . . . . . . . . . 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 598	. . . . . . . . . . . . 13 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
125	61, 67, 124	syl2anc 575	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
126	125	ex 399	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))))
127	8, 16, 24, 58, 126	finds2 7324	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))))
128	127	imp 395	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))
129	128	simprd 485	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))
130	129	expcom 400	. . . . . . 7 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))
131	130	ralrimdv 3156	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))
132	131	ralrimiv 3153	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚))
133		frn 6262	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ 𝑆)
134		ffun 6259	. . . . . . . . . . . . . . . 16 ⊢ (𝑠:suc 𝑛⟶𝐴 → Fun 𝑠)
135	134	3ad2ant1 1156	. . . . . . . . . . . . . . 15 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠)
136	135	rexlimivw 3217	. . . . . . . . . . . . . 14 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠)
137	136	ss2abi 3871	. . . . . . . . . . . . 13 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠}
138	28, 137	eqsstri 3832	. . . . . . . . . . . 12 ⊢ 𝑆 ⊆ {𝑠 ∣ Fun 𝑠}
139	133, 138	syl6ss 3810	. . . . . . . . . . 11 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ Fun 𝑠})
140	139	sseld 3797	. . . . . . . . . 10 ⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → 𝑢 ∈ {𝑠 ∣ Fun 𝑠}))
141		vex 3394	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
142		funeq 6121	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢))
143	141, 142	elab 3545	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢)
144	140, 143	syl6ib 242	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → Fun 𝑢))
145	144	adantr 468	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → Fun 𝑢))
146		ffn 6256	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → ℎ Fn ω)
147		fvelrnb 6464	. . . . . . . . . . . . 13 ⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ ↔ ∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣))
148		fvelrnb 6464	. . . . . . . . . . . . . . 15 ⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ ↔ ∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢))
149		nnord 7303	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ ω → Ord 𝑎)
150		nnord 7303	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ ω → Ord 𝑏)
151	149, 150	anim12i 602	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord 𝑎 ∧ Ord 𝑏))
152		ordtri3or 5968	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎))
153		fveq2 6408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑏 → (ℎ‘𝑚) = (ℎ‘𝑏))
154	153	sseq2d 3830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
155	154	raleqbi1dv 3335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑏 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
156	155	rspcv 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
157		fveq2 6408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑎 → (ℎ‘𝑗) = (ℎ‘𝑎))
158	157	sseq1d 3829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑏) ↔ (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))
159	158	rspccv 3499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))
160	156, 159	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))))
161	160	adantl 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))))
162	161	3imp 1130	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))
163	162	orcd 891	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
164	163	3exp 1141	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
165	164	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
166		fveq2 6408	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (ℎ‘𝑎) = (ℎ‘𝑏))
167		eqimss 3854	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))
168	167	orcd 891	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
169	166, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
170	169	2a1d 26	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
171		fveq2 6408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑎 → (ℎ‘𝑚) = (ℎ‘𝑎))
172	171	sseq2d 3830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
173	172	raleqbi1dv 3335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑎 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
174	173	rspcv 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
175		fveq2 6408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑏 → (ℎ‘𝑗) = (ℎ‘𝑏))
176	175	sseq1d 3829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑎) ↔ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
177	176	rspccv 3499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
178	174, 177	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
179	178	adantr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
180	179	3imp 1130	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))
181	180	olcd 892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
182	181	3exp 1141	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
183	182	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ 𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
184	165, 170, 183	3jaoi 1545	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
185	152, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord 𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
186	151, 185	mpcom 38	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
187		sseq12 3825	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ↔ 𝑢 ⊆ 𝑣))
188		sseq12 3825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ‘𝑏) = 𝑣 ∧ (ℎ‘𝑎) = 𝑢) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢))
189	188	ancoms 448	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢))
190	187, 189	orbi12d 933	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) ↔ (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
191	190	biimpcd 240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
192	186, 191	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
193	192	com23 86	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
194	193	exp4b 419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ω → (𝑏 ∈ ω → ((ℎ‘𝑎) = 𝑢 → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))))
195	194	com23 86	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ω → ((ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))))
196	195	rexlimiv 3215	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
197	196	rexlimdv 3218	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢 → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
198	148, 197	syl6bi 244	. . . . . . . . . . . . . 14 ⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
199	198	com23 86	. . . . . . . . . . . . 13 ⊢ (ℎ Fn ω → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
200	147, 199	sylbid 231	. . . . . . . . . . . 12 ⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
201	200	com24 95	. . . . . . . . . . 11 ⊢ (ℎ Fn ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
202	201	imp 395	. . . . . . . . . 10 ⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
203	202	ralrimdv 3156	. . . . . . . . 9 ⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
204	146, 203	sylan 571	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
205	145, 204	jcad 504	. . . . . . 7 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
206	205	ralrimiv 3153	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → ∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
207		fununi 6175	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → Fun ∪ ran ℎ)
208	206, 207	syl 17	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → Fun ∪ ran ℎ)
209	132, 208	syldan 581	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → Fun ∪ ran ℎ)
210		vex 3394	. . . . . . . . 9 ⊢ 𝑚 ∈ V
211	210	eldm2 5523	. . . . . . . 8 ⊢ (𝑚 ∈ dom ∪ ran ℎ ↔ ∃𝑢⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ)
212		eluni2 4634	. . . . . . . . . 10 ⊢ (⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ ↔ ∃𝑣 ∈ ran ℎ⟨𝑚, 𝑢⟩ ∈ 𝑣)
213	210, 141	opeldm 5529	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣)
214	213	a1i 11	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣))
215	133, 44	syl6ss 3810	. . . . . . . . . . . . . . 15 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
216		ssel 3792	. . . . . . . . . . . . . . . 16 ⊢ (ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran ℎ → 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
217		vex 3394	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑣 ∈ V
218		dmeq 5525	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣)
219	218	eleq2d 2871	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣))
220	218	eleq1d 2870	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω))
221	219, 220	anbi12d 618	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
222	217, 221	elab 3545	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))
223	222	simprbi 486	. . . . . . . . . . . . . . . 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 598	. . . . . . . . . . . . 13 ⊢ (ℎ:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
227		elnn 7305	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω)
228	226, 227	syl6 35	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → 𝑚 ∈ ω))
229	228	expcomd 404	. . . . . . . . . . 11 ⊢ (ℎ:ω⟶𝑆 → (𝑣 ∈ ran ℎ → (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ ω)))
230	229	rexlimdv 3218	. . . . . . . . . 10 ⊢ (ℎ:ω⟶𝑆 → (∃𝑣 ∈ ran ℎ⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ ω))
231	212, 230	syl5bi 233	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω))
232	231	exlimdv 2024	. . . . . . . 8 ⊢ (ℎ:ω⟶𝑆 → (∃𝑢⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω))
233	211, 232	syl5bi 233	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → (𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω))
234	233	adantr 468	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω))
235		id 22	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ω → 𝑚 ∈ ω)
236		fnfvelrn 6578	. . . . . . . . . . 11 ⊢ ((ℎ Fn ω ∧ 𝑚 ∈ ω) → (ℎ‘𝑚) ∈ ran ℎ)
237	146, 235, 236	syl2anr 586	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑚) ∈ ran ℎ)
238	237	adantrr 699	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑚) ∈ ran ℎ)
239	128	simpld 484	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom (ℎ‘𝑚))
240		dmeq 5525	. . . . . . . . . 10 ⊢ (𝑢 = (ℎ‘𝑚) → dom 𝑢 = dom (ℎ‘𝑚))
241	240	eliuni 4718	. . . . . . . . 9 ⊢ (((ℎ‘𝑚) ∈ ran ℎ ∧ 𝑚 ∈ dom (ℎ‘𝑚)) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎdom 𝑢)
242	238, 239, 241	syl2anc 575	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎdom 𝑢)
243		dmuni 5535	. . . . . . . 8 ⊢ dom ∪ ran ℎ = ∪ 𝑢 ∈ ran ℎdom 𝑢
244	242, 243	syl6eleqr 2896	. . . . . . 7 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom ∪ ran ℎ)
245	244	expcom 400	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ∪ ran ℎ))
246	234, 245	impbid 203	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran ℎ ↔ 𝑚 ∈ ω))
247	246	eqrdv 2804	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → dom ∪ ran ℎ = ω)
248		rnuni 5755	. . . . . 6 ⊢ ran ∪ ran ℎ = ∪ 𝑠 ∈ ran ℎran 𝑠
249		frn 6262	. . . . . . . . . . . . . 14 ⊢ (𝑠:suc 𝑛⟶𝐴 → ran 𝑠 ⊆ 𝐴)
250	249	3ad2ant1 1156	. . . . . . . . . . . . 13 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴)
251	250	rexlimivw 3217	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴)
252	251	ss2abi 3871	. . . . . . . . . . 11 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}
253	28, 252	eqsstri 3832	. . . . . . . . . 10 ⊢ 𝑆 ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}
254	133, 253	syl6ss 3810	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴})
255		ssel 3792	. . . . . . . . . 10 ⊢ (ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → 𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}))
256		abid 2794	. . . . . . . . . 10 ⊢ (𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} ↔ ran 𝑠 ⊆ 𝐴)
257	255, 256	syl6ib 242	. . . . . . . . 9 ⊢ (ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴))
258	254, 257	syl 17	. . . . . . . 8 ⊢ (ℎ:ω⟶𝑆 → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴))
259	258	ralrimiv 3153	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
260		iunss 4753	. . . . . . 7 ⊢ (∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴 ↔ ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
261	259, 260	sylibr 225	. . . . . 6 ⊢ (ℎ:ω⟶𝑆 → ∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
262	248, 261	syl5eqss 3846	. . . . 5 ⊢ (ℎ:ω⟶𝑆 → ran ∪ ran ℎ ⊆ 𝐴)
263	262	adantr 468	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ran ∪ ran ℎ ⊆ 𝐴)
264		df-fn 6104	. . . . 5 ⊢ (∪ ran ℎ Fn ω ↔ (Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω))
265		df-f 6105	. . . . . 6 ⊢ (∪ ran ℎ:ω⟶𝐴 ↔ (∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴))
266	265	biimpri 219	. . . . 5 ⊢ ((∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴)
267	264, 266	sylanbr 573	. . . 4 ⊢ (((Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω) ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴)
268	209, 247, 263, 267	syl21anc 857	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∪ ran ℎ:ω⟶𝐴)
269		fnfvelrn 6578	. . . . . . . 8 ⊢ ((ℎ Fn ω ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ ran ℎ)
270	146, 25, 269	sylancl 576	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ ran ℎ)
271	270	adantr 468	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ∈ ran ℎ)
272		elssuni 4661	. . . . . 6 ⊢ ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ⊆ ∪ ran ℎ)
273	271, 272	syl 17	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ⊆ ∪ ran ℎ)
274	54	adantr 468	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∅ ∈ dom (ℎ‘∅))
275		funssfv 6429	. . . . 5 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘∅) ⊆ ∪ ran ℎ ∧ ∅ ∈ dom (ℎ‘∅)) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅))
276	209, 273, 274, 275	syl3anc 1483	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅))
277		simp2 1160	. . . . . . . . . . 11 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶)
278	277	rexlimivw 3217	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶)
279	278	ss2abi 3871	. . . . . . . . 9 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
280	28, 279	eqsstri 3832	. . . . . . . 8 ⊢ 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
281	133, 280	syl6ss 3810	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶})
282		ssel 3792	. . . . . . . 8 ⊢ (ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶}))
283		fveq1 6407	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘∅) → (𝑠‘∅) = ((ℎ‘∅)‘∅))
284	283	eqeq1d 2808	. . . . . . . . 9 ⊢ (𝑠 = (ℎ‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((ℎ‘∅)‘∅) = 𝐶))
285	46, 284	elab 3545	. . . . . . . 8 ⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((ℎ‘∅)‘∅) = 𝐶)
286	282, 285	syl6ib 242	. . . . . . 7 ⊢ (ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
287	281, 286	syl 17	. . . . . 6 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
288	287	adantr 468	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
289	271, 288	mpd 15	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅)‘∅) = 𝐶)
290	276, 289	eqtrd 2840	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran ℎ‘∅) = 𝐶)
291		nfv 2005	. . . . 5 ⊢ Ⅎ𝑘 ℎ:ω⟶𝑆
292		nfra1 3129	. . . . 5 ⊢ Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))
293	291, 292	nfan 1990	. . . 4 ⊢ Ⅎ𝑘(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
294	133	ad2antrr 708	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ran ℎ ⊆ 𝑆)
295		peano2 7316	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
296		fnfvelrn 6578	. . . . . . . . 9 ⊢ ((ℎ Fn ω ∧ suc 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
297	146, 295, 296	syl2an 585	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
298	297	adantlr 697	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
299	239	expcom 400	. . . . . . . . 9 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (ℎ‘𝑚)))
300	299	ralrimiv 3153	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚))
301		id 22	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑘 → 𝑚 = suc 𝑘)
302		fveq2 6408	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑘 → (ℎ‘𝑚) = (ℎ‘suc 𝑘))
303	302	dmeqd 5527	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑘 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑘))
304	301, 303	eleq12d 2879	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑘 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
305	304	rspcv 3498	. . . . . . . . 9 ⊢ (suc 𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
306	295, 305	syl 17	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
307	300, 306	mpan9 498	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘))
308		eleq2 2874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (dom 𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛))
309	308	biimpa 464	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
310	29, 309	sylan 571	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
311		ordsucelsuc 7252	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑛 → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
312	30, 311	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ω → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
313	312	biimprd 239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛 → 𝑘 ∈ 𝑛))
314		rsp 3117	. . . . . . . . . . . . . . . . . . . . 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 399	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠:suc 𝑛⟶𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))))
319	318	com24 95	. . . . . . . . . . . . . . . 16 ⊢ (𝑠:suc 𝑛⟶𝐴 → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))))
320	319	imp 395	. . . . . . . . . . . . . . 15 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
321	320	3adant2 1154	. . . . . . . . . . . . . 14 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
322	321	impcom 396	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
323	322	rexlimiva 3216	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
324	323	ss2abi 3871	. . . . . . . . . . 11 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
325	28, 324	eqsstri 3832	. . . . . . . . . 10 ⊢ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
326		sstr 3806	. . . . . . . . . 10 ⊢ ((ran ℎ ⊆ 𝑆 ∧ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})
327	325, 326	mpan2 674	. . . . . . . . 9 ⊢ (ran ℎ ⊆ 𝑆 → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})
328	327	sseld 3797	. . . . . . . 8 ⊢ (ran ℎ ⊆ 𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}))
329		fvex 6421	. . . . . . . . 9 ⊢ (ℎ‘suc 𝑘) ∈ V
330		dmeq 5525	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → dom 𝑠 = dom (ℎ‘suc 𝑘))
331	330	eleq2d 2871	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
332		fveq1 6407	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
333		fveq1 6407	. . . . . . . . . . . 12 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
334	333	fveq2d 6412	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝐹‘(𝑠‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
335	332, 334	eleq12d 2879	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
336	331, 335	imbi12d 335	. . . . . . . . 9 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))))
337	329, 336	elab 3545	. . . . . . . 8 ⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
338	328, 337	syl6ib 242	. . . . . . 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 468	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → Fun ∪ ran ℎ)
341		elssuni 4661	. . . . . . . . . 10 ⊢ ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
342	297, 341	syl 17	. . . . . . . . 9 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
343	342	adantlr 697	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
344		funssfv 6429	. . . . . . . 8 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
345	340, 343, 307, 344	syl3anc 1483	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
346	215	sseld 3797	. . . . . . . . . . . . . . 15 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
347	330	eleq2d 2871	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘suc 𝑘)))
348	330	eleq1d 2870	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘suc 𝑘) ∈ ω))
349	347, 348	anbi12d 618	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
350	329, 349	elab 3545	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))
351	346, 350	syl6ib 242	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
352	351	adantr 468	. . . . . . . . . . . . 13 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
353	297, 352	mpd 15	. . . . . . . . . . . 12 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))
354	353	simprd 485	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → dom (ℎ‘suc 𝑘) ∈ ω)
355		nnord 7303	. . . . . . . . . . 11 ⊢ (dom (ℎ‘suc 𝑘) ∈ ω → Ord dom (ℎ‘suc 𝑘))
356		ordtr 5950	. . . . . . . . . . 11 ⊢ (Ord dom (ℎ‘suc 𝑘) → Tr dom (ℎ‘suc 𝑘))
357		trsuc 6023	. . . . . . . . . . . 12 ⊢ ((Tr dom (ℎ‘suc 𝑘) ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → 𝑘 ∈ dom (ℎ‘suc 𝑘))
358	357	ex 399	. . . . . . . . . . 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 697	. . . . . . . . 9 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘)))
361	307, 360	mpd 15	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom (ℎ‘suc 𝑘))
362		funssfv 6429	. . . . . . . 8 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ ∧ 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
363	340, 343, 361, 362	syl3anc 1483	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
364		simpl 470	. . . . . . . 8 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
365		simpr 473	. . . . . . . . 9 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
366	365	fveq2d 6412	. . . . . . . 8 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (𝐹‘(∪ ran ℎ‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
367	364, 366	eleq12d 2879	. . . . . . 7 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
368	345, 363, 367	syl2anc 575	. . . . . 6 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
369	339, 368	mpbird 248	. . . . 5 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))
370	369	ex 399	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑘 ∈ ω → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
371	293, 370	ralrimi 3145	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))
372		vex 3394	. . . . . 6 ⊢ ℎ ∈ V
373	372	rnex 7330	. . . . 5 ⊢ ran ℎ ∈ V
374	373	uniex 7183	. . . 4 ⊢ ∪ ran ℎ ∈ V
375		feq1 6237	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → (𝑔:ω⟶𝐴 ↔ ∪ ran ℎ:ω⟶𝐴))
376		fveq1 6407	. . . . . 6 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘∅) = (∪ ran ℎ‘∅))
377	376	eqeq1d 2808	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔‘∅) = 𝐶 ↔ (∪ ran ℎ‘∅) = 𝐶))
378		fveq1 6407	. . . . . . 7 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘suc 𝑘) = (∪ ran ℎ‘suc 𝑘))
379		fveq1 6407	. . . . . . . 8 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘𝑘) = (∪ ran ℎ‘𝑘))
380	379	fveq2d 6412	. . . . . . 7 ⊢ (𝑔 = ∪ ran ℎ → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(∪ ran ℎ‘𝑘)))
381	378, 380	eleq12d 2879	. . . . . 6 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
382	381	ralbidv 3174	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
383	375, 377, 382	3anbi123d 1553	. . . 4 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))))
384	374, 383	spcev 3493	. . 3 ⊢ ((∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
385	268, 290, 371, 384	syl3anc 1483	. 2 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
386	385	exlimiv 2021	1 ⊢ (∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∨ wo 865   ∨ w3o 1099   ∧ w3a 1100   = wceq 1637  ∃wex 1859   ∈ wcel 2156  {cab 2792  ∀wral 3096  ∃wrex 3097  {crab 3100  Vcvv 3391   ⊆ wss 3769  ∅c0 4116  ⟨cop 4376  ∪ cuni 4630  ∪ ciun 4712   ↦ cmpt 4923  Tr wtr 4946  dom cdm 5311  ran crn 5312   ↾ cres 5313  Ord word 5935  suc csuc 5938  Fun wfun 6095   Fn wfn 6096  ⟶wf 6097  ‘cfv 6101  ωcom 7295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-dc 9553

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fv 6109  df-om 7296  df-1o 7796

This theorem is referenced by:  axdc3lem4  9560