Theorem axdc3lem2 10453

Description: Lemma for axdc3 10456. 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 10448 (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 10448 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 23	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → 𝑚 = ∅)
2		fveq2 6888	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅))
3	2	dmeqd 5900	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → dom (ℎ‘𝑚) = dom (ℎ‘∅))
4	1, 3	eleq12d 2860	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑚 ∈ dom (ℎ‘𝑚) ↔ ∅ ∈ dom (ℎ‘∅)))
5		eleq2 2855	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ ∅))
6	2	sseq2d 3972	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘∅)))
7	5, 6	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
8	4, 7	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))))
9		id 23	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → 𝑚 = 𝑖)
10		fveq2 6888	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖))
11	10	dmeqd 5900	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘𝑖))
12	9, 11	eleq12d 2860	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ 𝑖 ∈ dom (ℎ‘𝑖)))
13		elequ2 2161	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ 𝑖))
14	10	sseq2d 3972	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))
15	13, 14	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))))
16	12, 15	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))))
17		id 23	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → 𝑚 = suc 𝑖)
18		fveq2 6888	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖))
19	18	dmeqd 5900	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑖))
20	17, 19	eleq12d 2860	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
21		eleq2 2855	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ suc 𝑖))
22	18	sseq2d 3972	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
23	21, 22	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
24	20, 23	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
25		peano1 7894	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
26		ffvelcdm 7083	. . . . . . . . . . . . . . 15 ⊢ ((ℎ:ω⟶𝑆 ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ 𝑆)
27	25, 26	mpan2 704	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ 𝑆)
28		axdc3lem2.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
29		fdm 6722	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠:suc 𝑛⟶𝐴 → dom 𝑠 = suc 𝑛)
30		nnord 7879	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ω → Ord 𝑛)
31		0elsuc 7840	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑛 → ∅ ∈ suc 𝑛)
32	30, 31	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → ∅ ∈ suc 𝑛)
33		peano2 7895	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
34		eleq2 2855	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛))
35		eleq1 2854	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω))
36	34, 35	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (dom 𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω)))
37	36	biimprcd 253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
38	32, 33, 37	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
39	29, 38	syl5com 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠:suc 𝑛⟶𝐴 → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
40	39	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
41	40	impcom 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
42	41	rexlimiva 3161	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
43	42	ss2abi 4023	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
44	28, 43	eqsstri 3986	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
45	44	sseli 3936	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘∅) ∈ 𝑆 → (ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
46		fvex 6901	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ‘∅) ∈ V
47		dmeq 5898	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = (ℎ‘∅) → dom 𝑠 = dom (ℎ‘∅))
48	47	eleq2d 2852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (ℎ‘∅) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘∅)))
49	47	eleq1d 2851	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (ℎ‘∅) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘∅) ∈ ω))
50	48, 49	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘∅) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω)))
51	46, 50	elab 3641	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω))
52	45, 51	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘∅) ∈ 𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω))
53	52	simpld 500	. . . . . . . . . . . . . 14 ⊢ ((ℎ‘∅) ∈ 𝑆 → ∅ ∈ dom (ℎ‘∅))
54	27, 53	syl 18	. . . . . . . . . . . . 13 ⊢ (ℎ:ω⟶𝑆 → ∅ ∈ dom (ℎ‘∅))
55		noel 4294	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑗 ∈ ∅
56	55	pm2.21i 120	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))
57	54, 56	jctir 530	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
58	57	adantr 486	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
59		ffvelcdm 7083	. . . . . . . . . . . . . . 15 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ 𝑆)
60	59	ancoms 464	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑖) ∈ 𝑆)
61	60	adantrr 730	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑖) ∈ 𝑆)
62		suceq 6436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
63	62	fveq2d 6892	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
64		2fveq3 6893	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖)))
65	63, 64	eleq12d 2860	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
66	65	rspcva 3582	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))
67	66	adantrl 729	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))
68	44	sseli 3936	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
69		fvex 6901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ‘𝑖) ∈ V
70		dmeq 5898	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (ℎ‘𝑖) → dom 𝑠 = dom (ℎ‘𝑖))
71	70	eleq2d 2852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (ℎ‘𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘𝑖)))
72	70	eleq1d 2851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (ℎ‘𝑖) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘𝑖) ∈ ω))
73	71, 72	anbi12d 644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (ℎ‘𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω)))
74	69, 73	elab 3641	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))
75	68, 74	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))
76	75	simprd 501	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → dom (ℎ‘𝑖) ∈ ω)
77		nnord 7879	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (ℎ‘𝑖) ∈ ω → Ord dom (ℎ‘𝑖))
78		ordsucelsuc 7827	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord dom (ℎ‘𝑖) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
79	76, 77, 78	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
80	79	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
81		dmeq 5898	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (ℎ‘𝑖) → dom 𝑥 = dom (ℎ‘𝑖))
82		suceq 6436	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑥 = dom (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖))
83	81, 82	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖))
84	83	eqeq2d 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (ℎ‘𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (ℎ‘𝑖)))
85	81	reseq2d 5983	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (ℎ‘𝑖)))
86		id 23	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → 𝑥 = (ℎ‘𝑖))
87	85, 86	eqeq12d 2782	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (ℎ‘𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
88	84, 87	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . 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 10452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑆 ∈ V
93	92	rabex 5314	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ∈ V
94	89, 90, 93	fvmpt 6996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝐺‘(ℎ‘𝑖)) = {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))})
95	94	eleq2d 2852	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))}))
96		dmeq 5898	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (ℎ‘suc 𝑖) → dom 𝑦 = dom (ℎ‘suc 𝑖))
97	96	eqeq1d 2768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (ℎ‘suc 𝑖) → (dom 𝑦 = suc dom (ℎ‘𝑖) ↔ dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖)))
98		reseq1 5977	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (ℎ‘suc 𝑖) → (𝑦 ↾ dom (ℎ‘𝑖)) = ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)))
99	98	eqeq1d 2768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (ℎ‘suc 𝑖) → ((𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) ↔ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
100	97, 99	anbi12d 644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (ℎ‘suc 𝑖) → ((dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)) ↔ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
101	100	elrab 3653	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
102	95, 101	bitrdi 290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))))
103	102	simplbda 505	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
104	103	simpld 500	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖))
105	104	eleq2d 2852	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
106	80, 105	bitr4d 285	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
107	106	biimpd 232	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) → suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
108	103	simprd 501	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))
109		resss 6005	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖)
110		sseq1 3965	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)))
111	109, 110	mpbii 236	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖))
112		elsuci 6437	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ suc 𝑖 → (𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖))
113		pm2.27 43	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))
114		sstr2 3947	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑗) ⊆ (ℎ‘𝑖) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
115	113, 114	syl6 36	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
116		fveq2 6888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑖 → (ℎ‘𝑗) = (ℎ‘𝑖))
117	116	sseq1d 3971	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)))
118	117	biimprd 251	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
119	118	a1d 26	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
120	115, 119	jaoi 871	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖) → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
121	112, 120	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ suc 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
122	121	com13 89	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
123	108, 111, 122	3syl 19	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
124	107, 123	anim12d 621	. . . . . . . . . . . . 13 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
125	61, 67, 124	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
126	125	ex 418	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))))
127	8, 16, 24, 58, 126	finds2 7904	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))))
128	127	imp 412	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))
129	128	simprd 501	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))
130	129	expcom 419	. . . . . . 7 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))
131	130	ralrimdv 3166	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))
132	131	ralrimiv 3159	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚))
133		frn 6720	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ 𝑆)
134		ffun 6715	. . . . . . . . . . . . . . . 16 ⊢ (𝑠:suc 𝑛⟶𝐴 → Fun 𝑠)
135	134	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠)
136	135	rexlimivw 3165	. . . . . . . . . . . . . 14 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠)
137	136	ss2abi 4023	. . . . . . . . . . . . 13 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠}
138	28, 137	eqsstri 3986	. . . . . . . . . . . 12 ⊢ 𝑆 ⊆ {𝑠 ∣ Fun 𝑠}
139	133, 138	sstrdi 3952	. . . . . . . . . . 11 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ Fun 𝑠})
140	139	sseld 3939	. . . . . . . . . 10 ⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → 𝑢 ∈ {𝑠 ∣ Fun 𝑠}))
141		vex 3462	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
142		funeq 6563	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢))
143	141, 142	elab 3641	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢)
144	140, 143	imbitrdi 254	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → Fun 𝑢))
145	144	adantr 486	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → Fun 𝑢))
146		ffn 6712	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → ℎ Fn ω)
147		fvelrnb 6948	. . . . . . . . . . . . 13 ⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ ↔ ∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣))
148		fvelrnb 6948	. . . . . . . . . . . . . . 15 ⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ ↔ ∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢))
149		nnord 7879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ ω → Ord 𝑎)
150		nnord 7879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ ω → Ord 𝑏)
151	149, 150	anim12i 625	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord 𝑎 ∧ Ord 𝑏))
152		ordtri3or 6400	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎))
153		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑏 → (ℎ‘𝑚) = (ℎ‘𝑏))
154	153	sseq2d 3972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
155	154	raleqbi1dv 3336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑏 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
156	155	rspcv 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
157		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑎 → (ℎ‘𝑗) = (ℎ‘𝑎))
158	157	sseq1d 3971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑏) ↔ (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))
159	158	rspccv 3581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))
160	156, 159	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))))
161	160	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))))
162	161	3imp 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))
163	162	orcd 887	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
164	163	3exp 1137	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
165	164	com3r 88	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
166		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (ℎ‘𝑎) = (ℎ‘𝑏))
167		eqimss 3998	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))
168	167	orcd 887	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
169	166, 168	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
170	169	2a1d 27	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
171		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑎 → (ℎ‘𝑚) = (ℎ‘𝑎))
172	171	sseq2d 3972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
173	172	raleqbi1dv 3336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑎 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
174	173	rspcv 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
175		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑏 → (ℎ‘𝑗) = (ℎ‘𝑏))
176	175	sseq1d 3971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑎) ↔ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
177	176	rspccv 3581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
178	174, 177	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
179	178	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
180	179	3imp 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))
181	180	olcd 888	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
182	181	3exp 1137	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
183	182	com3r 88	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ 𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
184	165, 170, 183	3jaoi 1454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
185	152, 184	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord 𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
186	151, 185	mpcom 39	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
187		sseq12 3967	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ↔ 𝑢 ⊆ 𝑣))
188		sseq12 3967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ‘𝑏) = 𝑣 ∧ (ℎ‘𝑎) = 𝑢) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢))
189	188	ancoms 464	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢))
190	187, 189	orbi12d 932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) ↔ (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
191	190	biimpcd 252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
192	186, 191	syl6 36	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
193	192	com23 87	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
194	193	exp4b 436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ω → (𝑏 ∈ ω → ((ℎ‘𝑎) = 𝑢 → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))))
195	194	com23 87	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ω → ((ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))))
196	195	rexlimiv 3162	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
197	196	rexlimdv 3167	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢 → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
198	148, 197	biimtrdi 256	. . . . . . . . . . . . . 14 ⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
199	198	com23 87	. . . . . . . . . . . . 13 ⊢ (ℎ Fn ω → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
200	147, 199	sylbid 243	. . . . . . . . . . . 12 ⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
201	200	com24 96	. . . . . . . . . . 11 ⊢ (ℎ Fn ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
202	201	imp 412	. . . . . . . . . 10 ⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
203	202	ralrimdv 3166	. . . . . . . . 9 ⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
204	146, 203	sylan 592	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
205	145, 204	jcad 522	. . . . . . 7 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
206	205	ralrimiv 3159	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → ∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
207		fununi 6618	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → Fun ∪ ran ℎ)
208	206, 207	syl 18	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → Fun ∪ ran ℎ)
209	132, 208	syldan 603	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → Fun ∪ ran ℎ)
210		vex 3462	. . . . . . . . 9 ⊢ 𝑚 ∈ V
211	210	eldm2 5896	. . . . . . . 8 ⊢ (𝑚 ∈ dom ∪ ran ℎ ↔ ∃𝑢⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ)
212		eluni2 4881	. . . . . . . . . 10 ⊢ (⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ ↔ ∃𝑣 ∈ ran ℎ⟨𝑚, 𝑢⟩ ∈ 𝑣)
213	210, 141	opeldm 5902	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣)
214	213	a1i 11	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣))
215	133, 44	sstrdi 3952	. . . . . . . . . . . . . . 15 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
216		ssel 3934	. . . . . . . . . . . . . . . 16 ⊢ (ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran ℎ → 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
217		vex 3462	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑣 ∈ V
218		dmeq 5898	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣)
219	218	eleq2d 2852	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣))
220	218	eleq1d 2851	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω))
221	219, 220	anbi12d 644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
222	217, 221	elab 3641	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))
223	222	simprbi 503	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → dom 𝑣 ∈ ω)
224	216, 223	syl6 36	. . . . . . . . . . . . . . 15 ⊢ (ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran ℎ → dom 𝑣 ∈ ω))
225	215, 224	syl 18	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (𝑣 ∈ ran ℎ → dom 𝑣 ∈ ω))
226	214, 225	anim12d 621	. . . . . . . . . . . . 13 ⊢ (ℎ:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
227		elnn 7882	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω)
228	226, 227	syl6 36	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → 𝑚 ∈ ω))
229	228	expcomd 422	. . . . . . . . . . 11 ⊢ (ℎ:ω⟶𝑆 → (𝑣 ∈ ran ℎ → (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ ω)))
230	229	rexlimdv 3167	. . . . . . . . . 10 ⊢ (ℎ:ω⟶𝑆 → (∃𝑣 ∈ ran ℎ⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ ω))
231	212, 230	biimtrid 245	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω))
232	231	exlimdv 1966	. . . . . . . 8 ⊢ (ℎ:ω⟶𝑆 → (∃𝑢⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω))
233	211, 232	biimtrid 245	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → (𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω))
234	233	adantr 486	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω))
235		id 23	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ω → 𝑚 ∈ ω)
236		fnfvelrn 7082	. . . . . . . . . . 11 ⊢ ((ℎ Fn ω ∧ 𝑚 ∈ ω) → (ℎ‘𝑚) ∈ ran ℎ)
237	146, 235, 236	syl2anr 609	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑚) ∈ ran ℎ)
238	237	adantrr 730	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑚) ∈ ran ℎ)
239	128	simpld 500	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom (ℎ‘𝑚))
240		dmeq 5898	. . . . . . . . . 10 ⊢ (𝑢 = (ℎ‘𝑚) → dom 𝑢 = dom (ℎ‘𝑚))
241	240	eliuni 4967	. . . . . . . . 9 ⊢ (((ℎ‘𝑚) ∈ ran ℎ ∧ 𝑚 ∈ dom (ℎ‘𝑚)) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎdom 𝑢)
242	238, 239, 241	syl2anc 596	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎdom 𝑢)
243		dmuni 5909	. . . . . . . 8 ⊢ dom ∪ ran ℎ = ∪ 𝑢 ∈ ran ℎdom 𝑢
244	242, 243	eleqtrrdi 2877	. . . . . . 7 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom ∪ ran ℎ)
245	244	expcom 419	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ∪ ran ℎ))
246	234, 245	impbid 215	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran ℎ ↔ 𝑚 ∈ ω))
247	246	eqrdv 2764	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → dom ∪ ran ℎ = ω)
248		rnuni 6151	. . . . . 6 ⊢ ran ∪ ran ℎ = ∪ 𝑠 ∈ ran ℎran 𝑠
249		frn 6720	. . . . . . . . . . . . . 14 ⊢ (𝑠:suc 𝑛⟶𝐴 → ran 𝑠 ⊆ 𝐴)
250	249	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴)
251	250	rexlimivw 3165	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴)
252	251	ss2abi 4023	. . . . . . . . . . 11 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}
253	28, 252	eqsstri 3986	. . . . . . . . . 10 ⊢ 𝑆 ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}
254	133, 253	sstrdi 3952	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴})
255		ssel 3934	. . . . . . . . . 10 ⊢ (ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → 𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}))
256		abid 2748	. . . . . . . . . 10 ⊢ (𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} ↔ ran 𝑠 ⊆ 𝐴)
257	255, 256	imbitrdi 254	. . . . . . . . 9 ⊢ (ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴))
258	254, 257	syl 18	. . . . . . . 8 ⊢ (ℎ:ω⟶𝑆 → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴))
259	258	ralrimiv 3159	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
260		iunss 5014	. . . . . . 7 ⊢ (∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴 ↔ ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
261	259, 260	sylibr 237	. . . . . 6 ⊢ (ℎ:ω⟶𝑆 → ∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
262	248, 261	eqsstrid 3978	. . . . 5 ⊢ (ℎ:ω⟶𝑆 → ran ∪ ran ℎ ⊆ 𝐴)
263	262	adantr 486	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ran ∪ ran ℎ ⊆ 𝐴)
264		df-fn 6546	. . . . 5 ⊢ (∪ ran ℎ Fn ω ↔ (Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω))
265		df-f 6547	. . . . . 6 ⊢ (∪ ran ℎ:ω⟶𝐴 ↔ (∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴))
266	265	biimpri 231	. . . . 5 ⊢ ((∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴)
267	264, 266	sylanbr 594	. . . 4 ⊢ (((Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω) ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴)
268	209, 247, 263, 267	syl21anc 851	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∪ ran ℎ:ω⟶𝐴)
269		fnfvelrn 7082	. . . . . . . 8 ⊢ ((ℎ Fn ω ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ ran ℎ)
270	146, 25, 269	sylancl 598	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ ran ℎ)
271	270	adantr 486	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ∈ ran ℎ)
272		elssuni 4909	. . . . . 6 ⊢ ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ⊆ ∪ ran ℎ)
273	271, 272	syl 18	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ⊆ ∪ ran ℎ)
274	54	adantr 486	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∅ ∈ dom (ℎ‘∅))
275		funssfv 6909	. . . . 5 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘∅) ⊆ ∪ ran ℎ ∧ ∅ ∈ dom (ℎ‘∅)) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅))
276	209, 273, 274, 275	syl3anc 1398	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅))
277		simp2 1155	. . . . . . . . . . 11 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶)
278	277	rexlimivw 3165	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶)
279	278	ss2abi 4023	. . . . . . . . 9 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
280	28, 279	eqsstri 3986	. . . . . . . 8 ⊢ 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
281	133, 280	sstrdi 3952	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶})
282		ssel 3934	. . . . . . . 8 ⊢ (ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶}))
283		fveq1 6887	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘∅) → (𝑠‘∅) = ((ℎ‘∅)‘∅))
284	283	eqeq1d 2768	. . . . . . . . 9 ⊢ (𝑠 = (ℎ‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((ℎ‘∅)‘∅) = 𝐶))
285	46, 284	elab 3641	. . . . . . . 8 ⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((ℎ‘∅)‘∅) = 𝐶)
286	282, 285	imbitrdi 254	. . . . . . 7 ⊢ (ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
287	281, 286	syl 18	. . . . . 6 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
288	287	adantr 486	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
289	271, 288	mpd 16	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅)‘∅) = 𝐶)
290	276, 289	eqtrd 2801	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran ℎ‘∅) = 𝐶)
291		nfv 1947	. . . . 5 ⊢ Ⅎ𝑘 ℎ:ω⟶𝑆
292		nfra1 3292	. . . . 5 ⊢ Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))
293	291, 292	nfan 1932	. . . 4 ⊢ Ⅎ𝑘(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
294	133	ad2antrr 739	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ran ℎ ⊆ 𝑆)
295		peano2 7895	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
296		fnfvelrn 7082	. . . . . . . . 9 ⊢ ((ℎ Fn ω ∧ suc 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
297	146, 295, 296	syl2an 608	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
298	297	adantlr 728	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
299	239	expcom 419	. . . . . . . . 9 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (ℎ‘𝑚)))
300	299	ralrimiv 3159	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚))
301		id 23	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑘 → 𝑚 = suc 𝑘)
302		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑘 → (ℎ‘𝑚) = (ℎ‘suc 𝑘))
303	302	dmeqd 5900	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑘 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑘))
304	301, 303	eleq12d 2860	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑘 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
305	304	rspcv 3580	. . . . . . . . 9 ⊢ (suc 𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
306	295, 305	syl 18	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
307	300, 306	mpan9 516	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘))
308		eleq2 2855	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (dom 𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛))
309	308	biimpa 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
310	29, 309	sylan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
311		ordsucelsuc 7827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑛 → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
312	30, 311	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ω → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
313	312	biimprd 251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛 → 𝑘 ∈ 𝑛))
314		rsp 3256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑘 ∈ 𝑛 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
315	313, 314	syl9r 79	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
316	315	com13 89	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑘 ∈ suc 𝑛 → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
317	310, 316	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
318	317	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠:suc 𝑛⟶𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))))
319	318	com24 96	. . . . . . . . . . . . . . . 16 ⊢ (𝑠:suc 𝑛⟶𝐴 → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))))
320	319	imp 412	. . . . . . . . . . . . . . 15 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
321	320	3adant2 1149	. . . . . . . . . . . . . 14 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
322	321	impcom 413	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
323	322	rexlimiva 3161	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
324	323	ss2abi 4023	. . . . . . . . . . 11 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
325	28, 324	eqsstri 3986	. . . . . . . . . 10 ⊢ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
326		sstr 3948	. . . . . . . . . 10 ⊢ ((ran ℎ ⊆ 𝑆 ∧ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})
327	325, 326	mpan2 704	. . . . . . . . 9 ⊢ (ran ℎ ⊆ 𝑆 → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})
328	327	sseld 3939	. . . . . . . 8 ⊢ (ran ℎ ⊆ 𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}))
329		fvex 6901	. . . . . . . . 9 ⊢ (ℎ‘suc 𝑘) ∈ V
330		dmeq 5898	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → dom 𝑠 = dom (ℎ‘suc 𝑘))
331	330	eleq2d 2852	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
332		fveq1 6887	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
333		fveq1 6887	. . . . . . . . . . . 12 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
334	333	fveq2d 6892	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝐹‘(𝑠‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
335	332, 334	eleq12d 2860	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
336	331, 335	imbi12d 347	. . . . . . . . 9 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))))
337	329, 336	elab 3641	. . . . . . . 8 ⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
338	328, 337	imbitrdi 254	. . . . . . 7 ⊢ (ran ℎ ⊆ 𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))))
339	294, 298, 307, 338	syl3c 67	. . . . . 6 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
340	209	adantr 486	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → Fun ∪ ran ℎ)
341		elssuni 4909	. . . . . . . . . 10 ⊢ ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
342	297, 341	syl 18	. . . . . . . . 9 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
343	342	adantlr 728	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
344		funssfv 6909	. . . . . . . 8 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
345	340, 343, 307, 344	syl3anc 1398	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
346	215	sseld 3939	. . . . . . . . . . . . . . 15 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
347	330	eleq2d 2852	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘suc 𝑘)))
348	330	eleq1d 2851	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘suc 𝑘) ∈ ω))
349	347, 348	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
350	329, 349	elab 3641	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))
351	346, 350	imbitrdi 254	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
352	351	adantr 486	. . . . . . . . . . . . 13 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
353	297, 352	mpd 16	. . . . . . . . . . . 12 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))
354	353	simprd 501	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → dom (ℎ‘suc 𝑘) ∈ ω)
355		nnord 7879	. . . . . . . . . . 11 ⊢ (dom (ℎ‘suc 𝑘) ∈ ω → Ord dom (ℎ‘suc 𝑘))
356		ordtr 6381	. . . . . . . . . . 11 ⊢ (Ord dom (ℎ‘suc 𝑘) → Tr dom (ℎ‘suc 𝑘))
357		trsuc 6457	. . . . . . . . . . . 12 ⊢ ((Tr dom (ℎ‘suc 𝑘) ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → 𝑘 ∈ dom (ℎ‘suc 𝑘))
358	357	ex 418	. . . . . . . . . . 11 ⊢ (Tr dom (ℎ‘suc 𝑘) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘)))
359	354, 355, 356, 358	4syl 20	. . . . . . . . . 10 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘)))
360	359	adantlr 728	. . . . . . . . 9 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘)))
361	307, 360	mpd 16	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom (ℎ‘suc 𝑘))
362		funssfv 6909	. . . . . . . 8 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ ∧ 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
363	340, 343, 361, 362	syl3anc 1398	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
364		simpl 488	. . . . . . . 8 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
365		simpr 490	. . . . . . . . 9 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
366	365	fveq2d 6892	. . . . . . . 8 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (𝐹‘(∪ ran ℎ‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
367	364, 366	eleq12d 2860	. . . . . . 7 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
368	345, 363, 367	syl2anc 596	. . . . . 6 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
369	339, 368	mpbird 260	. . . . 5 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))
370	369	ex 418	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑘 ∈ ω → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
371	293, 370	ralrimi 3266	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))
372		vex 3462	. . . . . 6 ⊢ ℎ ∈ V
373	372	rnex 7916	. . . . 5 ⊢ ran ℎ ∈ V
374	373	uniex 7752	. . . 4 ⊢ ∪ ran ℎ ∈ V
375		feq1 6690	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → (𝑔:ω⟶𝐴 ↔ ∪ ran ℎ:ω⟶𝐴))
376		fveq1 6887	. . . . . 6 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘∅) = (∪ ran ℎ‘∅))
377	376	eqeq1d 2768	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔‘∅) = 𝐶 ↔ (∪ ran ℎ‘∅) = 𝐶))
378		fveq1 6887	. . . . . . 7 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘suc 𝑘) = (∪ ran ℎ‘suc 𝑘))
379		fveq1 6887	. . . . . . . 8 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘𝑘) = (∪ ran ℎ‘𝑘))
380	379	fveq2d 6892	. . . . . . 7 ⊢ (𝑔 = ∪ ran ℎ → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(∪ ran ℎ‘𝑘)))
381	378, 380	eleq12d 2860	. . . . . 6 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
382	381	ralbidv 3191	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
383	375, 377, 382	3anbi123d 1464	. . . 4 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))))
384	374, 383	spcev 3568	. . 3 ⊢ ((∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
385	268, 290, 371, 384	syl3anc 1398	. 2 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
386	385	exlimiv 1963	1 ⊢ (∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2146  {cab 2744  ∀wral 3082  ∃wrex 3092  {crab 3419  Vcvv 3458   ⊆ wss 3908  ∅c0 4289  ⟨cop 4600  ∪ cuni 4877  ∪ ciun 4961   ↦ cmpt 5197  Tr wtr 5223  dom cdm 5666  ran crn 5667   ↾ cres 5668  Ord word 6366  suc csuc 6369  Fun wfun 6537   Fn wfn 6538  ⟶wf 6539  ‘cfv 6543  ωcom 7871

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-dc 10448

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-om 7872  df-1o 8462

This theorem is used by:  axdc3lem4  10455