Theorem tfrcllemaccex 6266

Description: We can define an acceptable function on any element of 𝑋.

As with many of the transfinite recursion theorems, we have hypotheses that state that 𝐹 is a function and that it is defined up to 𝑋. (Contributed by Jim Kingdon, 26-Mar-2022.)

Hypotheses

Ref	Expression
tfrcl.f	⊢ 𝐹 = recs(𝐺)
tfrcl.g	⊢ (𝜑 → Fun 𝐺)
tfrcl.x	⊢ (𝜑 → Ord 𝑋)
tfrcl.ex	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)
tfrcllemsucfn.1	⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}
tfrcllemaccex.u	⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)

Assertion

Ref	Expression
tfrcllemaccex	⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))

Distinct variable groups:   𝑢,𝐴,𝑥,𝑦   𝐶,𝑔,𝑢   𝑔,𝐺,𝑢,𝑦,𝑥   𝑓,𝐺,𝑥,𝑦   𝑆,𝑔,𝑢,𝑦,𝑥   𝑆,𝑓   𝑦,𝑋,𝑥,𝑓   𝜑,𝑦,𝑥,𝑓

Allowed substitution hints:   𝜑(𝑢,𝑔)   𝐴(𝑓,𝑔)   𝐶(𝑥,𝑦,𝑓)   𝐹(𝑥,𝑦,𝑢,𝑓,𝑔)   𝑋(𝑢,𝑔)

Proof of Theorem tfrcllemaccex

Dummy variables 𝑎 𝑏 𝑐 𝑟 𝑠 𝑡 𝑑 ℎ 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tfrcl.x	. . 3 ⊢ (𝜑 → Ord 𝑋)
2		ordelon 4313	. . 3 ⊢ ((Ord 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ On)
3	1, 2	sylan 281	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ On)
4		eleq1 2203	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝑋 ↔ 𝑤 ∈ 𝑋))
5	4	anbi2d 460	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝜑 ∧ 𝑧 ∈ 𝑋) ↔ (𝜑 ∧ 𝑤 ∈ 𝑋)))
6		feq2 5264	. . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑔:𝑧⟶𝑆 ↔ 𝑔:𝑤⟶𝑆))
7		raleq 2629	. . . . . 6 ⊢ (𝑧 = 𝑤 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
8	6, 7	anbi12d 465	. . . . 5 ⊢ (𝑧 = 𝑤 → ((𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
9	8	exbidv 1798	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
10	5, 9	imbi12d 233	. . 3 ⊢ (𝑧 = 𝑤 → (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
11		eleq1 2203	. . . . 5 ⊢ (𝑧 = 𝐶 → (𝑧 ∈ 𝑋 ↔ 𝐶 ∈ 𝑋))
12	11	anbi2d 460	. . . 4 ⊢ (𝑧 = 𝐶 → ((𝜑 ∧ 𝑧 ∈ 𝑋) ↔ (𝜑 ∧ 𝐶 ∈ 𝑋)))
13		feq2 5264	. . . . . 6 ⊢ (𝑧 = 𝐶 → (𝑔:𝑧⟶𝑆 ↔ 𝑔:𝐶⟶𝑆))
14		raleq 2629	. . . . . 6 ⊢ (𝑧 = 𝐶 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
15	13, 14	anbi12d 465	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
16	15	exbidv 1798	. . . 4 ⊢ (𝑧 = 𝐶 → (∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
17	12, 16	imbi12d 233	. . 3 ⊢ (𝑧 = 𝐶 → (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
18		tfrcl.f	. . . . . . . . 9 ⊢ 𝐹 = recs(𝐺)
19		tfrcl.g	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐺)
20	19	ad3antrrr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → Fun 𝐺)
21	1	ad3antrrr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → Ord 𝑋)
22		tfrcl.ex	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)
23	22	3expia 1184	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆))
24	23	alrimiv 1847	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑓(𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆))
25		feq1 5263	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → (𝑓:𝑥⟶𝑆 ↔ ℎ:𝑥⟶𝑆))
26		fveq2 5429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = ℎ → (𝐺‘𝑓) = (𝐺‘ℎ))
27	26	eleq1d 2209	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → ((𝐺‘𝑓) ∈ 𝑆 ↔ (𝐺‘ℎ) ∈ 𝑆))
28	25, 27	imbi12d 233	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → ((𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆) ↔ (ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆)))
29	28	cbvalv 1890	. . . . . . . . . . . . . . 15 ⊢ (∀𝑓(𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆) ↔ ∀ℎ(ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆))
30	24, 29	sylib 121	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀ℎ(ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆))
31	30	19.21bi 1538	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆))
32	31	3impia 1179	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
33	32	3adant1r 1210	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
34	33	3adant1r 1210	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
35	34	3adant1r 1210	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
36		tfrcllemsucfn.1	. . . . . . . . . 10 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}
37		fveq1 5428	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝑓‘𝑦) = (ℎ‘𝑦))
38		reseq1 4821	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → (𝑓 ↾ 𝑦) = (ℎ ↾ 𝑦))
39	38	fveq2d 5433	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝐺‘(𝑓 ↾ 𝑦)) = (𝐺‘(ℎ ↾ 𝑦)))
40	37, 39	eqeq12d 2155	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ℎ → ((𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦))))
41	40	ralbidv 2438	. . . . . . . . . . . . 13 ⊢ (𝑓 = ℎ → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦))))
42	25, 41	anbi12d 465	. . . . . . . . . . . 12 ⊢ (𝑓 = ℎ → ((𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))))
43	42	rexbidv 2439	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ 𝑋 (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))))
44	43	cbvabv 2265	. . . . . . . . . 10 ⊢ {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} = {ℎ ∣ ∃𝑥 ∈ 𝑋 (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))}
45	36, 44	eqtri 2161	. . . . . . . . 9 ⊢ 𝐴 = {ℎ ∣ ∃𝑥 ∈ 𝑋 (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))}
46		feq1 5263	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑟:𝑡⟶𝑆 ↔ 𝑎:𝑡⟶𝑆))
47		eleq1 2203	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑟 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
48		id 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑎 → 𝑟 = 𝑎)
49		fveq2 5429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑎 → (𝐺‘𝑟) = (𝐺‘𝑎))
50	49	opeq2d 3720	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑎 → ⟨𝑡, (𝐺‘𝑟)⟩ = ⟨𝑡, (𝐺‘𝑎)⟩)
51	50	sneqd 3545	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑎 → {⟨𝑡, (𝐺‘𝑟)⟩} = {⟨𝑡, (𝐺‘𝑎)⟩})
52	48, 51	uneq12d 3236	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑎 → (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}) = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}))
53	52	eqeq2d 2152	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
54	46, 47, 53	3anbi123d 1291	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑎 → ((𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ (𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}))))
55	54	cbvexv 1891	. . . . . . . . . . . . 13 ⊢ (∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
56	55	rexbii 2445	. . . . . . . . . . . 12 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑡 ∈ 𝑧 ∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
57		feq2 5264	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (𝑎:𝑡⟶𝑆 ↔ 𝑎:𝑏⟶𝑆))
58		opeq1 3713	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑏 → ⟨𝑡, (𝐺‘𝑎)⟩ = ⟨𝑏, (𝐺‘𝑎)⟩)
59	58	sneqd 3545	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → {⟨𝑡, (𝐺‘𝑎)⟩} = {⟨𝑏, (𝐺‘𝑎)⟩})
60	59	uneq2d 3235	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}) = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))
61	60	eqeq2d 2152	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
62	57, 61	3anbi13d 1293	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → ((𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ (𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
63	62	exbidv 1798	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑏 → (∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
64	63	cbvrexv 2658	. . . . . . . . . . . 12 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
65	56, 64	bitri 183	. . . . . . . . . . 11 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
66	65	abbii 2256	. . . . . . . . . 10 ⊢ {𝑠 ∣ ∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}))} = {𝑠 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
67		eqeq1 2147	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑑 → (𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}) ↔ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
68	67	3anbi3d 1297	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑑 → ((𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ (𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
69	68	exbidv 1798	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑑 → (∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
70	69	rexbidv 2439	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑑 → (∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
71	70	cbvabv 2265	. . . . . . . . . 10 ⊢ {𝑠 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))} = {𝑑 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
72	66, 71	eqtri 2161	. . . . . . . . 9 ⊢ {𝑠 ∣ ∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}))} = {𝑑 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
73		tfrcllemaccex.u	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
74	73	adantlr 469	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
75	74	adantlr 469	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
76	75	adantlr 469	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
77		simpr 109	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋)
78		simpr 109	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑏 ∈ 𝑧)
79		simplr 520	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑧 ∈ 𝑋)
80		ordtr1 4318	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑋 → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
81	1, 80	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
82	81	ad4antr 486	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
83	78, 79, 82	mp2and 430	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑏 ∈ 𝑋)
84		eleq1 2203	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑏 → (𝑤 ∈ 𝑋 ↔ 𝑏 ∈ 𝑋))
85		feq2 5264	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝑔:𝑤⟶𝑆 ↔ 𝑔:𝑏⟶𝑆))
86		raleq 2629	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
87	85, 86	anbi12d 465	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑏 → ((𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
88	87	exbidv 1798	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑏 → (∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
89	84, 88	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑏 → ((𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝑏 ∈ 𝑋 → ∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
90		simpllr 524	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
91	89, 90, 78	rspcdva 2798	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → (𝑏 ∈ 𝑋 → ∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
92		feq1 5263	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (𝑔:𝑏⟶𝑆 ↔ 𝑎:𝑏⟶𝑆))
93		fveq1 5428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑢) = (𝑎‘𝑢))
94		reseq1 4821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑎 → (𝑔 ↾ 𝑢) = (𝑎 ↾ 𝑢))
95	94	fveq2d 5433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → (𝐺‘(𝑔 ↾ 𝑢)) = (𝐺‘(𝑎 ↾ 𝑢)))
96	93, 95	eqeq12d 2155	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑎 → ((𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
97	96	ralbidv 2438	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
98	92, 97	anbi12d 465	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → ((𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)))))
99	98	cbvexv 1891	. . . . . . . . . . . . 13 ⊢ (∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
100		fveq2 5429	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑐 → (𝑎‘𝑢) = (𝑎‘𝑐))
101		reseq2 4822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑐 → (𝑎 ↾ 𝑢) = (𝑎 ↾ 𝑐))
102	101	fveq2d 5433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑐 → (𝐺‘(𝑎 ↾ 𝑢)) = (𝐺‘(𝑎 ↾ 𝑐)))
103	100, 102	eqeq12d 2155	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑐 → ((𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)) ↔ (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
104	103	cbvralv 2657	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)) ↔ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))
105	104	anbi2i 453	. . . . . . . . . . . . . 14 ⊢ ((𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))) ↔ (𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
106	105	exbii 1585	. . . . . . . . . . . . 13 ⊢ (∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
107	99, 106	bitri 183	. . . . . . . . . . . 12 ⊢ (∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
108	91, 107	syl6ib 160	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → (𝑏 ∈ 𝑋 → ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))))
109	83, 108	mpd 13	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
110	109	ralrimiva 2508	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∀𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
111	18, 20, 21, 35, 45, 72, 76, 77, 110	tfrcllemex 6265	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∃ℎ(ℎ:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))))
112		feq1 5263	. . . . . . . . . 10 ⊢ (ℎ = 𝑔 → (ℎ:𝑧⟶𝑆 ↔ 𝑔:𝑧⟶𝑆))
113		fveq1 5428	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (ℎ‘𝑢) = (𝑔‘𝑢))
114		reseq1 4821	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → (ℎ ↾ 𝑢) = (𝑔 ↾ 𝑢))
115	114	fveq2d 5433	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (𝐺‘(ℎ ↾ 𝑢)) = (𝐺‘(𝑔 ↾ 𝑢)))
116	113, 115	eqeq12d 2155	. . . . . . . . . . 11 ⊢ (ℎ = 𝑔 → ((ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢)) ↔ (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
117	116	ralbidv 2438	. . . . . . . . . 10 ⊢ (ℎ = 𝑔 → (∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
118	112, 117	anbi12d 465	. . . . . . . . 9 ⊢ (ℎ = 𝑔 → ((ℎ:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))) ↔ (𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
119	118	cbvexv 1891	. . . . . . . 8 ⊢ (∃ℎ(ℎ:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))) ↔ ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
120	111, 119	sylib 121	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
121	120	exp31 362	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
122	121	expcom 115	. . . . 5 ⊢ (𝑧 ∈ On → (𝜑 → (∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))))
123	122	a2d 26	. . . 4 ⊢ (𝑧 ∈ On → ((𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → (𝜑 → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))))
124		impexp 261	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
125	124	ralbii 2444	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ∀𝑤 ∈ 𝑧 (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
126		r19.21v 2512	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
127	125, 126	bitri 183	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
128		impexp 261	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
129	123, 127, 128	3imtr4g 204	. . 3 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → ((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
130	10, 17, 129	tfis3 4508	. 2 ⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
131	3, 130	mpcom 36	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963  ∀wal 1330   = wceq 1332  ∃wex 1469   ∈ wcel 1481  {cab 2126  ∀wral 2417  ∃wrex 2418   ∪ cun 3074  {csn 3532  ⟨cop 3535  ∪ cuni 3744  Ord word 4292  Oncon0 4293  suc csuc 4295   ↾ cres 4549  Fun wfun 5125  ⟶wf 5127  ‘cfv 5131  recscrecs 6209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4051  ax-sep 4054  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2914  df-csb 3008  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-nul 3369  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-iun 3823  df-br 3938  df-opab 3998  df-mpt 3999  df-tr 4035  df-id 4223  df-iord 4296  df-on 4298  df-suc 4301  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-fv 5139  df-recs 6210

This theorem is referenced by:  tfrcllemres  6267