Theorem axdc3lem2 10488

Description: Lemma for axdc3 10491. 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 10483 (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 10483 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 6906	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅))
3	2	dmeqd 5918	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → dom (ℎ‘𝑚) = dom (ℎ‘∅))
4	1, 3	eleq12d 2832	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑚 ∈ dom (ℎ‘𝑚) ↔ ∅ ∈ dom (ℎ‘∅)))
5		eleq2 2827	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ ∅))
6	2	sseq2d 4027	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘∅)))
7	5, 6	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
8	4, 7	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅)))))
9		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → 𝑚 = 𝑖)
10		fveq2 6906	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖))
11	10	dmeqd 5918	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘𝑖))
12	9, 11	eleq12d 2832	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ 𝑖 ∈ dom (ℎ‘𝑖)))
13		elequ2 2120	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ 𝑖))
14	10	sseq2d 4027	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))
15	13, 14	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))))
16	12, 15	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))))
17		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → 𝑚 = suc 𝑖)
18		fveq2 6906	. . . . . . . . . . . . . 14 ⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖))
19	18	dmeqd 5918	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑖))
20	17, 19	eleq12d 2832	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
21		eleq2 2827	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → (𝑗 ∈ 𝑚 ↔ 𝑗 ∈ suc 𝑖))
22	18	sseq2d 4027	. . . . . . . . . . . . 13 ⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
23	21, 22	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑖 → ((𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) ↔ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
24	20, 23	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑖 → ((𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))) ↔ (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
25		peano1 7910	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
26		ffvelcdm 7100	. . . . . . . . . . . . . . 15 ⊢ ((ℎ:ω⟶𝑆 ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ 𝑆)
27	25, 26	mpan2 691	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ 𝑆)
28		axdc3lem2.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
29		fdm 6745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠:suc 𝑛⟶𝐴 → dom 𝑠 = suc 𝑛)
30		nnord 7894	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ω → Ord 𝑛)
31		0elsuc 7854	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑛 → ∅ ∈ suc 𝑛)
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → ∅ ∈ suc 𝑛)
33		peano2 7912	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
34		eleq2 2827	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛))
35		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑠 = suc 𝑛 → (dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω))
36	34, 35	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (dom 𝑠 = suc 𝑛 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω)))
37	36	biimprcd 250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
38	32, 33, 37	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → (dom 𝑠 = suc 𝑛 → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
39	29, 38	syl5com 31	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠:suc 𝑛⟶𝐴 → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
40	39	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)))
41	40	impcom 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
42	41	rexlimiva 3144	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω))
43	42	ss2abi 4076	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
44	28, 43	eqsstri 4029	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}
45	44	sseli 3990	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘∅) ∈ 𝑆 → (ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
46		fvex 6919	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ‘∅) ∈ V
47		dmeq 5916	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = (ℎ‘∅) → dom 𝑠 = dom (ℎ‘∅))
48	47	eleq2d 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (ℎ‘∅) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘∅)))
49	47	eleq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (ℎ‘∅) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘∅) ∈ ω))
50	48, 49	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘∅) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω)))
51	46, 50	elab 3680	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω))
52	45, 51	sylib 218	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘∅) ∈ 𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ dom (ℎ‘∅) ∈ ω))
53	52	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((ℎ‘∅) ∈ 𝑆 → ∅ ∈ dom (ℎ‘∅))
54	27, 53	syl 17	. . . . . . . . . . . . 13 ⊢ (ℎ:ω⟶𝑆 → ∅ ∈ dom (ℎ‘∅))
55		noel 4343	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑗 ∈ ∅
56	55	pm2.21i 119	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))
57	54, 56	jctir 520	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
58	57	adantr 480	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∅ ∈ dom (ℎ‘∅) ∧ (𝑗 ∈ ∅ → (ℎ‘𝑗) ⊆ (ℎ‘∅))))
59		ffvelcdm 7100	. . . . . . . . . . . . . . 15 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ 𝑆)
60	59	ancoms 458	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑖) ∈ 𝑆)
61	60	adantrr 717	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑖) ∈ 𝑆)
62		suceq 6451	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
63	62	fveq2d 6910	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
64		2fveq3 6911	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖)))
65	63, 64	eleq12d 2832	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
66	65	rspcva 3619	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))
67	66	adantrl 716	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)))
68	44	sseli 3990	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
69		fvex 6919	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ‘𝑖) ∈ V
70		dmeq 5916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (ℎ‘𝑖) → dom 𝑠 = dom (ℎ‘𝑖))
71	70	eleq2d 2824	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (ℎ‘𝑖) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘𝑖)))
72	70	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (ℎ‘𝑖) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘𝑖) ∈ ω))
73	71, 72	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (ℎ‘𝑖) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω)))
74	69, 73	elab 3680	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))
75	68, 74	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (∅ ∈ dom (ℎ‘𝑖) ∧ dom (ℎ‘𝑖) ∈ ω))
76	75	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → dom (ℎ‘𝑖) ∈ ω)
77		nnord 7894	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (ℎ‘𝑖) ∈ ω → Ord dom (ℎ‘𝑖))
78		ordsucelsuc 7841	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord dom (ℎ‘𝑖) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
79	76, 77, 78	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
80	79	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
81		dmeq 5916	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (ℎ‘𝑖) → dom 𝑥 = dom (ℎ‘𝑖))
82		suceq 6451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑥 = dom (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖))
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → suc dom 𝑥 = suc dom (ℎ‘𝑖))
84	83	eqeq2d 2745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (ℎ‘𝑖) → (dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom (ℎ‘𝑖)))
85	81	reseq2d 5999	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → (𝑦 ↾ dom 𝑥) = (𝑦 ↾ dom (ℎ‘𝑖)))
86		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (ℎ‘𝑖) → 𝑥 = (ℎ‘𝑖))
87	85, 86	eqeq12d 2750	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (ℎ‘𝑖) → ((𝑦 ↾ dom 𝑥) = 𝑥 ↔ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
88	84, 87	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (ℎ‘𝑖) → ((dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥) ↔ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
89	88	rabbidv 3440	. . . . . . . . . . . . . . . . . . . . . 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 10487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑆 ∈ V
93	92	rabex 5344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ∈ V
94	89, 90, 93	fvmpt 7015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → (𝐺‘(ℎ‘𝑖)) = {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))})
95	94	eleq2d 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))}))
96		dmeq 5916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (ℎ‘suc 𝑖) → dom 𝑦 = dom (ℎ‘suc 𝑖))
97	96	eqeq1d 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (ℎ‘suc 𝑖) → (dom 𝑦 = suc dom (ℎ‘𝑖) ↔ dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖)))
98		reseq1 5993	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (ℎ‘suc 𝑖) → (𝑦 ↾ dom (ℎ‘𝑖)) = ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)))
99	98	eqeq1d 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (ℎ‘suc 𝑖) → ((𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) ↔ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
100	97, 99	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (ℎ‘suc 𝑖) → ((dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)) ↔ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
101	100	elrab 3694	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘suc 𝑖) ∈ {𝑦 ∈ 𝑆 ∣ (dom 𝑦 = suc dom (ℎ‘𝑖) ∧ (𝑦 ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))} ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))))
102	95, 101	bitrdi 287	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑖) ∈ 𝑆 → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ ((ℎ‘suc 𝑖) ∈ 𝑆 ∧ (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))))
103	102	simplbda 499	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖) ∧ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖)))
104	103	simpld 494	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → dom (ℎ‘suc 𝑖) = suc dom (ℎ‘𝑖))
105	104	eleq2d 2824	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ↔ suc 𝑖 ∈ suc dom (ℎ‘𝑖)))
106	80, 105	bitr4d 282	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) ↔ suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
107	106	biimpd 229	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → (𝑖 ∈ dom (ℎ‘𝑖) → suc 𝑖 ∈ dom (ℎ‘suc 𝑖)))
108	103	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖))
109		resss 6021	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖)
110		sseq1 4020	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)))
111	109, 110	mpbii 233	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘suc 𝑖) ↾ dom (ℎ‘𝑖)) = (ℎ‘𝑖) → (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖))
112		elsuci 6452	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ suc 𝑖 → (𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖))
113		pm2.27 42	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)))
114		sstr2 4001	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑗) ⊆ (ℎ‘𝑖) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
115	113, 114	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
116		fveq2 6906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑖 → (ℎ‘𝑗) = (ℎ‘𝑖))
117	116	sseq1d 4026	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → ((ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖) ↔ (ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖)))
118	117	biimprd 248	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))
119	118	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → ((𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖)) → ((ℎ‘𝑖) ⊆ (ℎ‘suc 𝑖) → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))
120	115, 119	jaoi 857	. . . . . . . . . . . . . . . . 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 609	. . . . . . . . . . . . 13 ⊢ (((ℎ‘𝑖) ∈ 𝑆 ∧ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
125	61, 67, 124	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖)))))
126	125	ex 412	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((𝑖 ∈ dom (ℎ‘𝑖) ∧ (𝑗 ∈ 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘𝑖))) → (suc 𝑖 ∈ dom (ℎ‘suc 𝑖) ∧ (𝑗 ∈ suc 𝑖 → (ℎ‘𝑗) ⊆ (ℎ‘suc 𝑖))))))
127	8, 16, 24, 58, 126	finds2 7920	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))))
128	127	imp 406	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ dom (ℎ‘𝑚) ∧ (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))
129	128	simprd 495	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))
130	129	expcom 413	. . . . . . 7 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → (𝑗 ∈ 𝑚 → (ℎ‘𝑗) ⊆ (ℎ‘𝑚))))
131	130	ralrimdv 3149	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)))
132	131	ralrimiv 3142	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚))
133		frn 6743	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ 𝑆)
134		ffun 6739	. . . . . . . . . . . . . . . 16 ⊢ (𝑠:suc 𝑛⟶𝐴 → Fun 𝑠)
135	134	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠)
136	135	rexlimivw 3148	. . . . . . . . . . . . . 14 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → Fun 𝑠)
137	136	ss2abi 4076	. . . . . . . . . . . . 13 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ Fun 𝑠}
138	28, 137	eqsstri 4029	. . . . . . . . . . . 12 ⊢ 𝑆 ⊆ {𝑠 ∣ Fun 𝑠}
139	133, 138	sstrdi 4007	. . . . . . . . . . 11 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ Fun 𝑠})
140	139	sseld 3993	. . . . . . . . . 10 ⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → 𝑢 ∈ {𝑠 ∣ Fun 𝑠}))
141		vex 3481	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
142		funeq 6587	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑢 → (Fun 𝑠 ↔ Fun 𝑢))
143	141, 142	elab 3680	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑠 ∣ Fun 𝑠} ↔ Fun 𝑢)
144	140, 143	imbitrdi 251	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → (𝑢 ∈ ran ℎ → Fun 𝑢))
145	144	adantr 480	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → Fun 𝑢))
146		ffn 6736	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → ℎ Fn ω)
147		fvelrnb 6968	. . . . . . . . . . . . 13 ⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ ↔ ∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣))
148		fvelrnb 6968	. . . . . . . . . . . . . . 15 ⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ ↔ ∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢))
149		nnord 7894	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ ω → Ord 𝑎)
150		nnord 7894	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ ω → Ord 𝑏)
151	149, 150	anim12i 613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (Ord 𝑎 ∧ Ord 𝑏))
152		ordtri3or 6417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Ord 𝑎 ∧ Ord 𝑏) → (𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎))
153		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑏 → (ℎ‘𝑚) = (ℎ‘𝑏))
154	153	sseq2d 4027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
155	154	raleqbi1dv 3335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑏 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
156	155	rspcv 3617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏)))
157		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑎 → (ℎ‘𝑗) = (ℎ‘𝑎))
158	157	sseq1d 4026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑏) ↔ (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))
159	158	rspccv 3618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑗 ∈ 𝑏 (ℎ‘𝑗) ⊆ (ℎ‘𝑏) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏)))
160	156, 159	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))))
161	160	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))))
162	161	3imp 1110	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))
163	162	orcd 873	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑎 ∈ 𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
164	163	3exp 1118	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑎 ∈ 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
165	164	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 ∈ 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
166		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (ℎ‘𝑎) = (ℎ‘𝑏))
167		eqimss 4053	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → (ℎ‘𝑎) ⊆ (ℎ‘𝑏))
168	167	orcd 873	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘𝑎) = (ℎ‘𝑏) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
169	166, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑏 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
170	169	2a1d 26	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑏 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
171		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = 𝑎 → (ℎ‘𝑚) = (ℎ‘𝑎))
172	171	sseq2d 4027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = 𝑎 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
173	172	raleqbi1dv 3335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = 𝑎 → (∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ↔ ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
174	173	rspcv 3617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎)))
175		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑏 → (ℎ‘𝑗) = (ℎ‘𝑏))
176	175	sseq1d 4026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑏 → ((ℎ‘𝑗) ⊆ (ℎ‘𝑎) ↔ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
177	176	rspccv 3618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑗 ∈ 𝑎 (ℎ‘𝑗) ⊆ (ℎ‘𝑎) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
178	174, 177	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 ∈ ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
179	178	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
180	179	3imp 1110	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → (ℎ‘𝑏) ⊆ (ℎ‘𝑎))
181	180	olcd 874	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) ∧ 𝑏 ∈ 𝑎) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))
182	181	3exp 1118	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑏 ∈ 𝑎 → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
183	182	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ 𝑎 → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
184	165, 170, 183	3jaoi 1427	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
185	152, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord 𝑎 ∧ Ord 𝑏) → ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)))))
186	151, 185	mpcom 38	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎))))
187		sseq12 4022	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ↔ 𝑢 ⊆ 𝑣))
188		sseq12 4022	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ‘𝑏) = 𝑣 ∧ (ℎ‘𝑎) = 𝑢) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢))
189	188	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → ((ℎ‘𝑏) ⊆ (ℎ‘𝑎) ↔ 𝑣 ⊆ 𝑢))
190	187, 189	orbi12d 918	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) ↔ (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
191	190	biimpcd 249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ‘𝑎) ⊆ (ℎ‘𝑏) ∨ (ℎ‘𝑏) ⊆ (ℎ‘𝑎)) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
192	186, 191	syl6 35	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
193	192	com23 86	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (((ℎ‘𝑎) = 𝑢 ∧ (ℎ‘𝑏) = 𝑣) → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
194	193	exp4b 430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ω → (𝑏 ∈ ω → ((ℎ‘𝑎) = 𝑢 → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))))
195	194	com23 86	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ω → ((ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))))
196	195	rexlimiv 3145	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢 → (𝑏 ∈ ω → ((ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
197	196	rexlimdv 3150	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎 ∈ ω (ℎ‘𝑎) = 𝑢 → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
198	148, 197	biimtrdi 253	. . . . . . . . . . . . . 14 ⊢ (ℎ Fn ω → (𝑢 ∈ ran ℎ → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
199	198	com23 86	. . . . . . . . . . . . 13 ⊢ (ℎ Fn ω → (∃𝑏 ∈ ω (ℎ‘𝑏) = 𝑣 → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
200	147, 199	sylbid 240	. . . . . . . . . . . 12 ⊢ (ℎ Fn ω → (𝑣 ∈ ran ℎ → (𝑢 ∈ ran ℎ → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
201	200	com24 95	. . . . . . . . . . 11 ⊢ (ℎ Fn ω → (∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))))
202	201	imp 406	. . . . . . . . . 10 ⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (𝑣 ∈ ran ℎ → (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
203	202	ralrimdv 3149	. . . . . . . . 9 ⊢ ((ℎ Fn ω ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
204	146, 203	sylan 580	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
205	145, 204	jcad 512	. . . . . . 7 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → (𝑢 ∈ ran ℎ → (Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))))
206	205	ralrimiv 3142	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → ∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))
207		fununi 6642	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℎ(Fun 𝑢 ∧ ∀𝑣 ∈ ran ℎ(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → Fun ∪ ran ℎ)
208	206, 207	syl 17	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑚 ∈ ω ∀𝑗 ∈ 𝑚 (ℎ‘𝑗) ⊆ (ℎ‘𝑚)) → Fun ∪ ran ℎ)
209	132, 208	syldan 591	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → Fun ∪ ran ℎ)
210		vex 3481	. . . . . . . . 9 ⊢ 𝑚 ∈ V
211	210	eldm2 5914	. . . . . . . 8 ⊢ (𝑚 ∈ dom ∪ ran ℎ ↔ ∃𝑢⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ)
212		eluni2 4915	. . . . . . . . . 10 ⊢ (⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ ↔ ∃𝑣 ∈ ran ℎ⟨𝑚, 𝑢⟩ ∈ 𝑣)
213	210, 141	opeldm 5920	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣)
214	213	a1i 11	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ dom 𝑣))
215	133, 44	sstrdi 4007	. . . . . . . . . . . . . . 15 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)})
216		ssel 3988	. . . . . . . . . . . . . . . 16 ⊢ (ran ℎ ⊆ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} → (𝑣 ∈ ran ℎ → 𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
217		vex 3481	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑣 ∈ V
218		dmeq 5916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑣 → dom 𝑠 = dom 𝑣)
219	218	eleq2d 2824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑣 → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣))
220	218	eleq1d 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑣 → (dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω))
221	219, 220	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑣 → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
222	217, 221	elab 3680	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω))
223	222	simprbi 496	. . . . . . . . . . . . . . . 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 609	. . . . . . . . . . . . 13 ⊢ (ℎ:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → (𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω)))
227		elnn 7897	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω) → 𝑚 ∈ ω)
228	226, 227	syl6 35	. . . . . . . . . . . 12 ⊢ (ℎ:ω⟶𝑆 → ((⟨𝑚, 𝑢⟩ ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ) → 𝑚 ∈ ω))
229	228	expcomd 416	. . . . . . . . . . 11 ⊢ (ℎ:ω⟶𝑆 → (𝑣 ∈ ran ℎ → (⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ ω)))
230	229	rexlimdv 3150	. . . . . . . . . 10 ⊢ (ℎ:ω⟶𝑆 → (∃𝑣 ∈ ran ℎ⟨𝑚, 𝑢⟩ ∈ 𝑣 → 𝑚 ∈ ω))
231	212, 230	biimtrid 242	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → (⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω))
232	231	exlimdv 1930	. . . . . . . 8 ⊢ (ℎ:ω⟶𝑆 → (∃𝑢⟨𝑚, 𝑢⟩ ∈ ∪ ran ℎ → 𝑚 ∈ ω))
233	211, 232	biimtrid 242	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → (𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω))
234	233	adantr 480	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω))
235		id 22	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ω → 𝑚 ∈ ω)
236		fnfvelrn 7099	. . . . . . . . . . 11 ⊢ ((ℎ Fn ω ∧ 𝑚 ∈ ω) → (ℎ‘𝑚) ∈ ran ℎ)
237	146, 235, 236	syl2anr 597	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ω ∧ ℎ:ω⟶𝑆) → (ℎ‘𝑚) ∈ ran ℎ)
238	237	adantrr 717	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (ℎ‘𝑚) ∈ ran ℎ)
239	128	simpld 494	. . . . . . . . 9 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom (ℎ‘𝑚))
240		dmeq 5916	. . . . . . . . . 10 ⊢ (𝑢 = (ℎ‘𝑚) → dom 𝑢 = dom (ℎ‘𝑚))
241	240	eliuni 5001	. . . . . . . . 9 ⊢ (((ℎ‘𝑚) ∈ ran ℎ ∧ 𝑚 ∈ dom (ℎ‘𝑚)) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎdom 𝑢)
242	238, 239, 241	syl2anc 584	. . . . . . . 8 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎdom 𝑢)
243		dmuni 5927	. . . . . . . 8 ⊢ dom ∪ ran ℎ = ∪ 𝑢 ∈ ran ℎdom 𝑢
244	242, 243	eleqtrrdi 2849	. . . . . . 7 ⊢ ((𝑚 ∈ ω ∧ (ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → 𝑚 ∈ dom ∪ ran ℎ)
245	244	expcom 413	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom ∪ ran ℎ))
246	234, 245	impbid 212	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ dom ∪ ran ℎ ↔ 𝑚 ∈ ω))
247	246	eqrdv 2732	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → dom ∪ ran ℎ = ω)
248		rnuni 6170	. . . . . 6 ⊢ ran ∪ ran ℎ = ∪ 𝑠 ∈ ran ℎran 𝑠
249		frn 6743	. . . . . . . . . . . . . 14 ⊢ (𝑠:suc 𝑛⟶𝐴 → ran 𝑠 ⊆ 𝐴)
250	249	3ad2ant1 1132	. . . . . . . . . . . . 13 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴)
251	250	rexlimivw 3148	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → ran 𝑠 ⊆ 𝐴)
252	251	ss2abi 4076	. . . . . . . . . . 11 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}
253	28, 252	eqsstri 4029	. . . . . . . . . 10 ⊢ 𝑆 ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}
254	133, 253	sstrdi 4007	. . . . . . . . 9 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴})
255		ssel 3988	. . . . . . . . . 10 ⊢ (ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → 𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴}))
256		abid 2715	. . . . . . . . . 10 ⊢ (𝑠 ∈ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} ↔ ran 𝑠 ⊆ 𝐴)
257	255, 256	imbitrdi 251	. . . . . . . . 9 ⊢ (ran ℎ ⊆ {𝑠 ∣ ran 𝑠 ⊆ 𝐴} → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴))
258	254, 257	syl 17	. . . . . . . 8 ⊢ (ℎ:ω⟶𝑆 → (𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴))
259	258	ralrimiv 3142	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
260		iunss 5049	. . . . . . 7 ⊢ (∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴 ↔ ∀𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
261	259, 260	sylibr 234	. . . . . 6 ⊢ (ℎ:ω⟶𝑆 → ∪ 𝑠 ∈ ran ℎran 𝑠 ⊆ 𝐴)
262	248, 261	eqsstrid 4043	. . . . 5 ⊢ (ℎ:ω⟶𝑆 → ran ∪ ran ℎ ⊆ 𝐴)
263	262	adantr 480	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ran ∪ ran ℎ ⊆ 𝐴)
264		df-fn 6565	. . . . 5 ⊢ (∪ ran ℎ Fn ω ↔ (Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω))
265		df-f 6566	. . . . . 6 ⊢ (∪ ran ℎ:ω⟶𝐴 ↔ (∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴))
266	265	biimpri 228	. . . . 5 ⊢ ((∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴)
267	264, 266	sylanbr 582	. . . 4 ⊢ (((Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω) ∧ ran ∪ ran ℎ ⊆ 𝐴) → ∪ ran ℎ:ω⟶𝐴)
268	209, 247, 263, 267	syl21anc 838	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∪ ran ℎ:ω⟶𝐴)
269		fnfvelrn 7099	. . . . . . . 8 ⊢ ((ℎ Fn ω ∧ ∅ ∈ ω) → (ℎ‘∅) ∈ ran ℎ)
270	146, 25, 269	sylancl 586	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → (ℎ‘∅) ∈ ran ℎ)
271	270	adantr 480	. . . . . 6 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ∈ ran ℎ)
272		elssuni 4941	. . . . . 6 ⊢ ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ⊆ ∪ ran ℎ)
273	271, 272	syl 17	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (ℎ‘∅) ⊆ ∪ ran ℎ)
274	54	adantr 480	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∅ ∈ dom (ℎ‘∅))
275		funssfv 6927	. . . . 5 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘∅) ⊆ ∪ ran ℎ ∧ ∅ ∈ dom (ℎ‘∅)) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅))
276	209, 273, 274, 275	syl3anc 1370	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran ℎ‘∅) = ((ℎ‘∅)‘∅))
277		simp2 1136	. . . . . . . . . . 11 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶)
278	277	rexlimivw 3148	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑠‘∅) = 𝐶)
279	278	ss2abi 4076	. . . . . . . . 9 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
280	28, 279	eqsstri 4029	. . . . . . . 8 ⊢ 𝑆 ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶}
281	133, 280	sstrdi 4007	. . . . . . 7 ⊢ (ℎ:ω⟶𝑆 → ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶})
282		ssel 3988	. . . . . . . 8 ⊢ (ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → (ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶}))
283		fveq1 6905	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘∅) → (𝑠‘∅) = ((ℎ‘∅)‘∅))
284	283	eqeq1d 2736	. . . . . . . . 9 ⊢ (𝑠 = (ℎ‘∅) → ((𝑠‘∅) = 𝐶 ↔ ((ℎ‘∅)‘∅) = 𝐶))
285	46, 284	elab 3680	. . . . . . . 8 ⊢ ((ℎ‘∅) ∈ {𝑠 ∣ (𝑠‘∅) = 𝐶} ↔ ((ℎ‘∅)‘∅) = 𝐶)
286	282, 285	imbitrdi 251	. . . . . . 7 ⊢ (ran ℎ ⊆ {𝑠 ∣ (𝑠‘∅) = 𝐶} → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
287	281, 286	syl 17	. . . . . 6 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
288	287	adantr 480	. . . . 5 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅) ∈ ran ℎ → ((ℎ‘∅)‘∅) = 𝐶))
289	271, 288	mpd 15	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((ℎ‘∅)‘∅) = 𝐶)
290	276, 289	eqtrd 2774	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (∪ ran ℎ‘∅) = 𝐶)
291		nfv 1911	. . . . 5 ⊢ Ⅎ𝑘 ℎ:ω⟶𝑆
292		nfra1 3281	. . . . 5 ⊢ Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))
293	291, 292	nfan 1896	. . . 4 ⊢ Ⅎ𝑘(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
294	133	ad2antrr 726	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ran ℎ ⊆ 𝑆)
295		peano2 7912	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
296		fnfvelrn 7099	. . . . . . . . 9 ⊢ ((ℎ Fn ω ∧ suc 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
297	146, 295, 296	syl2an 596	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
298	297	adantlr 715	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ ran ℎ)
299	239	expcom 413	. . . . . . . . 9 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑚 ∈ ω → 𝑚 ∈ dom (ℎ‘𝑚)))
300	299	ralrimiv 3142	. . . . . . . 8 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚))
301		id 22	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑘 → 𝑚 = suc 𝑘)
302		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑚 = suc 𝑘 → (ℎ‘𝑚) = (ℎ‘suc 𝑘))
303	302	dmeqd 5918	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑘 → dom (ℎ‘𝑚) = dom (ℎ‘suc 𝑘))
304	301, 303	eleq12d 2832	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑘 → (𝑚 ∈ dom (ℎ‘𝑚) ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
305	304	rspcv 3617	. . . . . . . . 9 ⊢ (suc 𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
306	295, 305	syl 17	. . . . . . . 8 ⊢ (𝑘 ∈ ω → (∀𝑚 ∈ ω 𝑚 ∈ dom (ℎ‘𝑚) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
307	300, 306	mpan9 506	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ dom (ℎ‘suc 𝑘))
308		eleq2 2827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (dom 𝑠 = suc 𝑛 → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛))
309	308	biimpa 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
310	29, 309	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ suc 𝑘 ∈ dom 𝑠) → suc 𝑘 ∈ suc 𝑛)
311		ordsucelsuc 7841	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑛 → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
312	30, 311	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ω → (𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛))
313	312	biimprd 248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ω → (suc 𝑘 ∈ suc 𝑛 → 𝑘 ∈ 𝑛))
314		rsp 3244	. . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠:suc 𝑛⟶𝐴 → (suc 𝑘 ∈ dom 𝑠 → (𝑛 ∈ ω → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))))
319	318	com24 95	. . . . . . . . . . . . . . . 16 ⊢ (𝑠:suc 𝑛⟶𝐴 → (∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))))
320	319	imp 406	. . . . . . . . . . . . . . 15 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
321	320	3adant2 1130	. . . . . . . . . . . . . 14 ⊢ ((𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (𝑛 ∈ ω → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
322	321	impcom 407	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
323	322	rexlimiva 3144	. . . . . . . . . . . 12 ⊢ (∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) → (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
324	323	ss2abi 4076	. . . . . . . . . . 11 ⊢ {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
325	28, 324	eqsstri 4029	. . . . . . . . . 10 ⊢ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
326		sstr 4003	. . . . . . . . . 10 ⊢ ((ran ℎ ⊆ 𝑆 ∧ 𝑆 ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}) → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})
327	325, 326	mpan2 691	. . . . . . . . 9 ⊢ (ran ℎ ⊆ 𝑆 → ran ℎ ⊆ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))})
328	327	sseld 3993	. . . . . . . 8 ⊢ (ran ℎ ⊆ 𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}))
329		fvex 6919	. . . . . . . . 9 ⊢ (ℎ‘suc 𝑘) ∈ V
330		dmeq 5916	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → dom 𝑠 = dom (ℎ‘suc 𝑘))
331	330	eleq2d 2824	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)))
332		fveq1 6905	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
333		fveq1 6905	. . . . . . . . . . . 12 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝑠‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
334	333	fveq2d 6910	. . . . . . . . . . 11 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (𝐹‘(𝑠‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
335	332, 334	eleq12d 2832	. . . . . . . . . 10 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
336	331, 335	imbi12d 344	. . . . . . . . 9 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))) ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))))
337	329, 336	elab 3680	. . . . . . . 8 ⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (suc 𝑘 ∈ dom 𝑠 → (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))} ↔ (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
338	328, 337	imbitrdi 251	. . . . . . 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 480	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → Fun ∪ ran ℎ)
341		elssuni 4941	. . . . . . . . . 10 ⊢ ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
342	297, 341	syl 17	. . . . . . . . 9 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
343	342	adantlr 715	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ)
344		funssfv 6927	. . . . . . . 8 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
345	340, 343, 307, 344	syl3anc 1370	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
346	215	sseld 3993	. . . . . . . . . . . . . . 15 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)}))
347	330	eleq2d 2824	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (∅ ∈ dom 𝑠 ↔ ∅ ∈ dom (ℎ‘suc 𝑘)))
348	330	eleq1d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (ℎ‘suc 𝑘) → (dom 𝑠 ∈ ω ↔ dom (ℎ‘suc 𝑘) ∈ ω))
349	347, 348	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (ℎ‘suc 𝑘) → ((∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω) ↔ (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
350	329, 349	elab 3680	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘suc 𝑘) ∈ {𝑠 ∣ (∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω)} ↔ (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))
351	346, 350	imbitrdi 251	. . . . . . . . . . . . . 14 ⊢ (ℎ:ω⟶𝑆 → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
352	351	adantr 480	. . . . . . . . . . . . 13 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ran ℎ → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω)))
353	297, 352	mpd 15	. . . . . . . . . . . 12 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → (∅ ∈ dom (ℎ‘suc 𝑘) ∧ dom (ℎ‘suc 𝑘) ∈ ω))
354	353	simprd 495	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶𝑆 ∧ 𝑘 ∈ ω) → dom (ℎ‘suc 𝑘) ∈ ω)
355		nnord 7894	. . . . . . . . . . 11 ⊢ (dom (ℎ‘suc 𝑘) ∈ ω → Ord dom (ℎ‘suc 𝑘))
356		ordtr 6399	. . . . . . . . . . 11 ⊢ (Ord dom (ℎ‘suc 𝑘) → Tr dom (ℎ‘suc 𝑘))
357		trsuc 6472	. . . . . . . . . . . 12 ⊢ ((Tr dom (ℎ‘suc 𝑘) ∧ suc 𝑘 ∈ dom (ℎ‘suc 𝑘)) → 𝑘 ∈ dom (ℎ‘suc 𝑘))
358	357	ex 412	. . . . . . . . . . 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 715	. . . . . . . . 9 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (suc 𝑘 ∈ dom (ℎ‘suc 𝑘) → 𝑘 ∈ dom (ℎ‘suc 𝑘)))
361	307, 360	mpd 15	. . . . . . . 8 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ dom (ℎ‘suc 𝑘))
362		funssfv 6927	. . . . . . . 8 ⊢ ((Fun ∪ ran ℎ ∧ (ℎ‘suc 𝑘) ⊆ ∪ ran ℎ ∧ 𝑘 ∈ dom (ℎ‘suc 𝑘)) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
363	340, 343, 361, 362	syl3anc 1370	. . . . . . 7 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
364		simpl 482	. . . . . . . 8 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘))
365		simpr 484	. . . . . . . . 9 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘))
366	365	fveq2d 6910	. . . . . . . 8 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → (𝐹‘(∪ ran ℎ‘𝑘)) = (𝐹‘((ℎ‘suc 𝑘)‘𝑘)))
367	364, 366	eleq12d 2832	. . . . . . 7 ⊢ (((∪ ran ℎ‘suc 𝑘) = ((ℎ‘suc 𝑘)‘suc 𝑘) ∧ (∪ ran ℎ‘𝑘) = ((ℎ‘suc 𝑘)‘𝑘)) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
368	345, 363, 367	syl2anc 584	. . . . . 6 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)) ↔ ((ℎ‘suc 𝑘)‘suc 𝑘) ∈ (𝐹‘((ℎ‘suc 𝑘)‘𝑘))))
369	339, 368	mpbird 257	. . . . 5 ⊢ (((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))
370	369	ex 412	. . . 4 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑘 ∈ ω → (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
371	293, 370	ralrimi 3254	. . 3 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))
372		vex 3481	. . . . . 6 ⊢ ℎ ∈ V
373	372	rnex 7932	. . . . 5 ⊢ ran ℎ ∈ V
374	373	uniex 7759	. . . 4 ⊢ ∪ ran ℎ ∈ V
375		feq1 6716	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → (𝑔:ω⟶𝐴 ↔ ∪ ran ℎ:ω⟶𝐴))
376		fveq1 6905	. . . . . 6 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘∅) = (∪ ran ℎ‘∅))
377	376	eqeq1d 2736	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔‘∅) = 𝐶 ↔ (∪ ran ℎ‘∅) = 𝐶))
378		fveq1 6905	. . . . . . 7 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘suc 𝑘) = (∪ ran ℎ‘suc 𝑘))
379		fveq1 6905	. . . . . . . 8 ⊢ (𝑔 = ∪ ran ℎ → (𝑔‘𝑘) = (∪ ran ℎ‘𝑘))
380	379	fveq2d 6910	. . . . . . 7 ⊢ (𝑔 = ∪ ran ℎ → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(∪ ran ℎ‘𝑘)))
381	378, 380	eleq12d 2832	. . . . . 6 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
382	381	ralbidv 3175	. . . . 5 ⊢ (𝑔 = ∪ ran ℎ → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))))
383	375, 377, 382	3anbi123d 1435	. . . 4 ⊢ (𝑔 = ∪ ran ℎ → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘)))))
384	374, 383	spcev 3605	. . 3 ⊢ ((∪ ran ℎ:ω⟶𝐴 ∧ (∪ ran ℎ‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (∪ ran ℎ‘suc 𝑘) ∈ (𝐹‘(∪ ran ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
385	268, 290, 371, 384	syl3anc 1370	. 2 ⊢ ((ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
386	385	exlimiv 1927	1 ⊢ (∃ℎ(ℎ:ω⟶𝑆 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   ∧ w3a 1086   = wceq 1536  ∃wex 1775   ∈ wcel 2105  {cab 2711  ∀wral 3058  ∃wrex 3067  {crab 3432  Vcvv 3477   ⊆ wss 3962  ∅c0 4338  ⟨cop 4636  ∪ cuni 4911  ∪ ciun 4995   ↦ cmpt 5230  Tr wtr 5264  dom cdm 5688  ran crn 5689   ↾ cres 5690  Ord word 6384  suc csuc 6387  Fun wfun 6556   Fn wfn 6557  ⟶wf 6558  ‘cfv 6562  ωcom 7886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-dc 10483

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-om 7887  df-1o 8504

This theorem is referenced by:  axdc3lem4  10490