Theorem tfrcllemaccex 6416

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 4415	. . 3 ⊢ ((Ord 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ On)
3	1, 2	sylan 283	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ On)
4		eleq1 2256	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝑋 ↔ 𝑤 ∈ 𝑋))
5	4	anbi2d 464	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝜑 ∧ 𝑧 ∈ 𝑋) ↔ (𝜑 ∧ 𝑤 ∈ 𝑋)))
6		feq2 5388	. . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑔:𝑧⟶𝑆 ↔ 𝑔:𝑤⟶𝑆))
7		raleq 2690	. . . . . 6 ⊢ (𝑧 = 𝑤 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
8	6, 7	anbi12d 473	. . . . 5 ⊢ (𝑧 = 𝑤 → ((𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
9	8	exbidv 1836	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
10	5, 9	imbi12d 234	. . 3 ⊢ (𝑧 = 𝑤 → (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
11		eleq1 2256	. . . . 5 ⊢ (𝑧 = 𝐶 → (𝑧 ∈ 𝑋 ↔ 𝐶 ∈ 𝑋))
12	11	anbi2d 464	. . . 4 ⊢ (𝑧 = 𝐶 → ((𝜑 ∧ 𝑧 ∈ 𝑋) ↔ (𝜑 ∧ 𝐶 ∈ 𝑋)))
13		feq2 5388	. . . . . 6 ⊢ (𝑧 = 𝐶 → (𝑔:𝑧⟶𝑆 ↔ 𝑔:𝐶⟶𝑆))
14		raleq 2690	. . . . . 6 ⊢ (𝑧 = 𝐶 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
15	13, 14	anbi12d 473	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
16	15	exbidv 1836	. . . 4 ⊢ (𝑧 = 𝐶 → (∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
17	12, 16	imbi12d 234	. . 3 ⊢ (𝑧 = 𝐶 → (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
18		tfrcl.f	. . . . . . . . 9 ⊢ 𝐹 = recs(𝐺)
19		tfrcl.g	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐺)
20	19	ad3antrrr 492	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → Fun 𝐺)
21	1	ad3antrrr 492	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → Ord 𝑋)
22		tfrcl.ex	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆)
23	22	3expia 1207	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆))
24	23	alrimiv 1885	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑓(𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆))
25		feq1 5387	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → (𝑓:𝑥⟶𝑆 ↔ ℎ:𝑥⟶𝑆))
26		fveq2 5555	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = ℎ → (𝐺‘𝑓) = (𝐺‘ℎ))
27	26	eleq1d 2262	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → ((𝐺‘𝑓) ∈ 𝑆 ↔ (𝐺‘ℎ) ∈ 𝑆))
28	25, 27	imbi12d 234	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → ((𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆) ↔ (ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆)))
29	28	cbvalv 1929	. . . . . . . . . . . . . . 15 ⊢ (∀𝑓(𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆) ↔ ∀ℎ(ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆))
30	24, 29	sylib 122	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀ℎ(ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆))
31	30	19.21bi 1569	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆))
32	31	3impia 1202	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
33	32	3adant1r 1233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
34	33	3adant1r 1233	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
35	34	3adant1r 1233	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
36		tfrcllemsucfn.1	. . . . . . . . . 10 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}
37		fveq1 5554	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝑓‘𝑦) = (ℎ‘𝑦))
38		reseq1 4937	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → (𝑓 ↾ 𝑦) = (ℎ ↾ 𝑦))
39	38	fveq2d 5559	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝐺‘(𝑓 ↾ 𝑦)) = (𝐺‘(ℎ ↾ 𝑦)))
40	37, 39	eqeq12d 2208	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ℎ → ((𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦))))
41	40	ralbidv 2494	. . . . . . . . . . . . 13 ⊢ (𝑓 = ℎ → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦))))
42	25, 41	anbi12d 473	. . . . . . . . . . . 12 ⊢ (𝑓 = ℎ → ((𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))))
43	42	rexbidv 2495	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ 𝑋 (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))))
44	43	cbvabv 2318	. . . . . . . . . 10 ⊢ {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} = {ℎ ∣ ∃𝑥 ∈ 𝑋 (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))}
45	36, 44	eqtri 2214	. . . . . . . . 9 ⊢ 𝐴 = {ℎ ∣ ∃𝑥 ∈ 𝑋 (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))}
46		feq1 5387	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑟:𝑡⟶𝑆 ↔ 𝑎:𝑡⟶𝑆))
47		eleq1 2256	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑟 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
48		id 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑎 → 𝑟 = 𝑎)
49		fveq2 5555	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑎 → (𝐺‘𝑟) = (𝐺‘𝑎))
50	49	opeq2d 3812	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑎 → ⟨𝑡, (𝐺‘𝑟)⟩ = ⟨𝑡, (𝐺‘𝑎)⟩)
51	50	sneqd 3632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑎 → {⟨𝑡, (𝐺‘𝑟)⟩} = {⟨𝑡, (𝐺‘𝑎)⟩})
52	48, 51	uneq12d 3315	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑎 → (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}) = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}))
53	52	eqeq2d 2205	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
54	46, 47, 53	3anbi123d 1323	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑎 → ((𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ (𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}))))
55	54	cbvexv 1930	. . . . . . . . . . . . 13 ⊢ (∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
56	55	rexbii 2501	. . . . . . . . . . . 12 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑡 ∈ 𝑧 ∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
57		feq2 5388	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (𝑎:𝑡⟶𝑆 ↔ 𝑎:𝑏⟶𝑆))
58		opeq1 3805	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑏 → ⟨𝑡, (𝐺‘𝑎)⟩ = ⟨𝑏, (𝐺‘𝑎)⟩)
59	58	sneqd 3632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → {⟨𝑡, (𝐺‘𝑎)⟩} = {⟨𝑏, (𝐺‘𝑎)⟩})
60	59	uneq2d 3314	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}) = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))
61	60	eqeq2d 2205	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
62	57, 61	3anbi13d 1325	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → ((𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ (𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
63	62	exbidv 1836	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑏 → (∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
64	63	cbvrexv 2727	. . . . . . . . . . . 12 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
65	56, 64	bitri 184	. . . . . . . . . . 11 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
66	65	abbii 2309	. . . . . . . . . 10 ⊢ {𝑠 ∣ ∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}))} = {𝑠 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
67		eqeq1 2200	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑑 → (𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}) ↔ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
68	67	3anbi3d 1329	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑑 → ((𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ (𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
69	68	exbidv 1836	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑑 → (∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
70	69	rexbidv 2495	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑑 → (∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
71	70	cbvabv 2318	. . . . . . . . . 10 ⊢ {𝑠 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))} = {𝑑 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
72	66, 71	eqtri 2214	. . . . . . . . 9 ⊢ {𝑠 ∣ ∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}))} = {𝑑 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
73		tfrcllemaccex.u	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
74	73	adantlr 477	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
75	74	adantlr 477	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
76	75	adantlr 477	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
77		simpr 110	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋)
78		simpr 110	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑏 ∈ 𝑧)
79		simplr 528	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑧 ∈ 𝑋)
80		ordtr1 4420	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑋 → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
81	1, 80	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
82	81	ad4antr 494	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
83	78, 79, 82	mp2and 433	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑏 ∈ 𝑋)
84		eleq1 2256	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑏 → (𝑤 ∈ 𝑋 ↔ 𝑏 ∈ 𝑋))
85		feq2 5388	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝑔:𝑤⟶𝑆 ↔ 𝑔:𝑏⟶𝑆))
86		raleq 2690	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
87	85, 86	anbi12d 473	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑏 → ((𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
88	87	exbidv 1836	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑏 → (∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
89	84, 88	imbi12d 234	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑏 → ((𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝑏 ∈ 𝑋 → ∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
90		simpllr 534	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
91	89, 90, 78	rspcdva 2870	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → (𝑏 ∈ 𝑋 → ∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
92		feq1 5387	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (𝑔:𝑏⟶𝑆 ↔ 𝑎:𝑏⟶𝑆))
93		fveq1 5554	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑢) = (𝑎‘𝑢))
94		reseq1 4937	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑎 → (𝑔 ↾ 𝑢) = (𝑎 ↾ 𝑢))
95	94	fveq2d 5559	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → (𝐺‘(𝑔 ↾ 𝑢)) = (𝐺‘(𝑎 ↾ 𝑢)))
96	93, 95	eqeq12d 2208	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑎 → ((𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
97	96	ralbidv 2494	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
98	92, 97	anbi12d 473	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → ((𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)))))
99	98	cbvexv 1930	. . . . . . . . . . . . 13 ⊢ (∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
100		fveq2 5555	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑐 → (𝑎‘𝑢) = (𝑎‘𝑐))
101		reseq2 4938	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑐 → (𝑎 ↾ 𝑢) = (𝑎 ↾ 𝑐))
102	101	fveq2d 5559	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑐 → (𝐺‘(𝑎 ↾ 𝑢)) = (𝐺‘(𝑎 ↾ 𝑐)))
103	100, 102	eqeq12d 2208	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑐 → ((𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)) ↔ (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
104	103	cbvralv 2726	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)) ↔ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))
105	104	anbi2i 457	. . . . . . . . . . . . . 14 ⊢ ((𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))) ↔ (𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
106	105	exbii 1616	. . . . . . . . . . . . 13 ⊢ (∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
107	99, 106	bitri 184	. . . . . . . . . . . 12 ⊢ (∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
108	91, 107	imbitrdi 161	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → (𝑏 ∈ 𝑋 → ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))))
109	83, 108	mpd 13	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
110	109	ralrimiva 2567	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∀𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
111	18, 20, 21, 35, 45, 72, 76, 77, 110	tfrcllemex 6415	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∃ℎ(ℎ:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))))
112		feq1 5387	. . . . . . . . . 10 ⊢ (ℎ = 𝑔 → (ℎ:𝑧⟶𝑆 ↔ 𝑔:𝑧⟶𝑆))
113		fveq1 5554	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (ℎ‘𝑢) = (𝑔‘𝑢))
114		reseq1 4937	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → (ℎ ↾ 𝑢) = (𝑔 ↾ 𝑢))
115	114	fveq2d 5559	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (𝐺‘(ℎ ↾ 𝑢)) = (𝐺‘(𝑔 ↾ 𝑢)))
116	113, 115	eqeq12d 2208	. . . . . . . . . . 11 ⊢ (ℎ = 𝑔 → ((ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢)) ↔ (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
117	116	ralbidv 2494	. . . . . . . . . 10 ⊢ (ℎ = 𝑔 → (∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
118	112, 117	anbi12d 473	. . . . . . . . 9 ⊢ (ℎ = 𝑔 → ((ℎ:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))) ↔ (𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
119	118	cbvexv 1930	. . . . . . . 8 ⊢ (∃ℎ(ℎ:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))) ↔ ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
120	111, 119	sylib 122	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
121	120	exp31 364	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
122	121	expcom 116	. . . . 5 ⊢ (𝑧 ∈ On → (𝜑 → (∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))))
123	122	a2d 26	. . . 4 ⊢ (𝑧 ∈ On → ((𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → (𝜑 → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))))
124		impexp 263	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
125	124	ralbii 2500	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ∀𝑤 ∈ 𝑧 (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
126		r19.21v 2571	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
127	125, 126	bitri 184	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
128		impexp 263	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
129	123, 127, 128	3imtr4g 205	. . 3 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → ((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
130	10, 17, 129	tfis3 4619	. 2 ⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
131	3, 130	mpcom 36	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980  ∀wal 1362   = wceq 1364  ∃wex 1503   ∈ wcel 2164  {cab 2179  ∀wral 2472  ∃wrex 2473   ∪ cun 3152  {csn 3619  ⟨cop 3622  ∪ cuni 3836  Ord word 4394  Oncon0 4395  suc csuc 4397   ↾ cres 4662  Fun wfun 5249  ⟶wf 5251  ‘cfv 5255  recscrecs 6359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4145  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-csb 3082  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3448  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-iun 3915  df-br 4031  df-opab 4092  df-mpt 4093  df-tr 4129  df-id 4325  df-iord 4398  df-on 4400  df-suc 4403  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-rn 4671  df-res 4672  df-ima 4673  df-iota 5216  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-recs 6360

This theorem is referenced by:  tfrcllemres  6417