Theorem tfrcllemaccex 6505

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 4473	. . 3 ⊢ ((Ord 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ On)
3	1, 2	sylan 283	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ On)
4		eleq1 2292	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝑋 ↔ 𝑤 ∈ 𝑋))
5	4	anbi2d 464	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝜑 ∧ 𝑧 ∈ 𝑋) ↔ (𝜑 ∧ 𝑤 ∈ 𝑋)))
6		feq2 5456	. . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑔:𝑧⟶𝑆 ↔ 𝑔:𝑤⟶𝑆))
7		raleq 2728	. . . . . 6 ⊢ (𝑧 = 𝑤 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
8	6, 7	anbi12d 473	. . . . 5 ⊢ (𝑧 = 𝑤 → ((𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
9	8	exbidv 1871	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
10	5, 9	imbi12d 234	. . 3 ⊢ (𝑧 = 𝑤 → (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
11		eleq1 2292	. . . . 5 ⊢ (𝑧 = 𝐶 → (𝑧 ∈ 𝑋 ↔ 𝐶 ∈ 𝑋))
12	11	anbi2d 464	. . . 4 ⊢ (𝑧 = 𝐶 → ((𝜑 ∧ 𝑧 ∈ 𝑋) ↔ (𝜑 ∧ 𝐶 ∈ 𝑋)))
13		feq2 5456	. . . . . 6 ⊢ (𝑧 = 𝐶 → (𝑔:𝑧⟶𝑆 ↔ 𝑔:𝐶⟶𝑆))
14		raleq 2728	. . . . . 6 ⊢ (𝑧 = 𝐶 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
15	13, 14	anbi12d 473	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
16	15	exbidv 1871	. . . 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 1229	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆))
24	23	alrimiv 1920	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑓(𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆))
25		feq1 5455	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → (𝑓:𝑥⟶𝑆 ↔ ℎ:𝑥⟶𝑆))
26		fveq2 5626	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = ℎ → (𝐺‘𝑓) = (𝐺‘ℎ))
27	26	eleq1d 2298	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → ((𝐺‘𝑓) ∈ 𝑆 ↔ (𝐺‘ℎ) ∈ 𝑆))
28	25, 27	imbi12d 234	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → ((𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆) ↔ (ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆)))
29	28	cbvalv 1964	. . . . . . . . . . . . . . 15 ⊢ (∀𝑓(𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆) ↔ ∀ℎ(ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆))
30	24, 29	sylib 122	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀ℎ(ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆))
31	30	19.21bi 1604	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (ℎ:𝑥⟶𝑆 → (𝐺‘ℎ) ∈ 𝑆))
32	31	3impia 1224	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
33	32	3adant1r 1255	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
34	33	3adant1r 1255	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
35	34	3adant1r 1255	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝑋 ∧ ℎ:𝑥⟶𝑆) → (𝐺‘ℎ) ∈ 𝑆)
36		tfrcllemsucfn.1	. . . . . . . . . 10 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}
37		fveq1 5625	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝑓‘𝑦) = (ℎ‘𝑦))
38		reseq1 4998	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → (𝑓 ↾ 𝑦) = (ℎ ↾ 𝑦))
39	38	fveq2d 5630	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝐺‘(𝑓 ↾ 𝑦)) = (𝐺‘(ℎ ↾ 𝑦)))
40	37, 39	eqeq12d 2244	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ℎ → ((𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦))))
41	40	ralbidv 2530	. . . . . . . . . . . . 13 ⊢ (𝑓 = ℎ → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦))))
42	25, 41	anbi12d 473	. . . . . . . . . . . 12 ⊢ (𝑓 = ℎ → ((𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))))
43	42	rexbidv 2531	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ 𝑋 (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))))
44	43	cbvabv 2354	. . . . . . . . . 10 ⊢ {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} = {ℎ ∣ ∃𝑥 ∈ 𝑋 (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))}
45	36, 44	eqtri 2250	. . . . . . . . 9 ⊢ 𝐴 = {ℎ ∣ ∃𝑥 ∈ 𝑋 (ℎ:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))}
46		feq1 5455	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑟:𝑡⟶𝑆 ↔ 𝑎:𝑡⟶𝑆))
47		eleq1 2292	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑟 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
48		id 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑎 → 𝑟 = 𝑎)
49		fveq2 5626	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑎 → (𝐺‘𝑟) = (𝐺‘𝑎))
50	49	opeq2d 3863	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑎 → ⟨𝑡, (𝐺‘𝑟)⟩ = ⟨𝑡, (𝐺‘𝑎)⟩)
51	50	sneqd 3679	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑎 → {⟨𝑡, (𝐺‘𝑟)⟩} = {⟨𝑡, (𝐺‘𝑎)⟩})
52	48, 51	uneq12d 3359	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑎 → (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}) = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}))
53	52	eqeq2d 2241	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
54	46, 47, 53	3anbi123d 1346	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑎 → ((𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ (𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}))))
55	54	cbvexv 1965	. . . . . . . . . . . . 13 ⊢ (∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
56	55	rexbii 2537	. . . . . . . . . . . 12 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑡 ∈ 𝑧 ∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
57		feq2 5456	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (𝑎:𝑡⟶𝑆 ↔ 𝑎:𝑏⟶𝑆))
58		opeq1 3856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑏 → ⟨𝑡, (𝐺‘𝑎)⟩ = ⟨𝑏, (𝐺‘𝑎)⟩)
59	58	sneqd 3679	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → {⟨𝑡, (𝐺‘𝑎)⟩} = {⟨𝑏, (𝐺‘𝑎)⟩})
60	59	uneq2d 3358	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}) = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))
61	60	eqeq2d 2241	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
62	57, 61	3anbi13d 1348	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → ((𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ (𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
63	62	exbidv 1871	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑏 → (∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
64	63	cbvrexv 2766	. . . . . . . . . . . 12 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑎(𝑎:𝑡⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
65	56, 64	bitri 184	. . . . . . . . . . 11 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
66	65	abbii 2345	. . . . . . . . . 10 ⊢ {𝑠 ∣ ∃𝑡 ∈ 𝑧 ∃𝑟(𝑟:𝑡⟶𝑆 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}))} = {𝑠 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
67		eqeq1 2236	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑑 → (𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}) ↔ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
68	67	3anbi3d 1352	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑑 → ((𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ (𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
69	68	exbidv 1871	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑑 → (∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
70	69	rexbidv 2531	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑑 → (∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
71	70	cbvabv 2354	. . . . . . . . . 10 ⊢ {𝑠 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))} = {𝑑 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
72	66, 71	eqtri 2250	. . . . . . . . 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 4478	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑋 → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
81	1, 80	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
82	81	ad4antr 494	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
83	78, 79, 82	mp2and 433	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑏 ∈ 𝑋)
84		eleq1 2292	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑏 → (𝑤 ∈ 𝑋 ↔ 𝑏 ∈ 𝑋))
85		feq2 5456	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝑔:𝑤⟶𝑆 ↔ 𝑔:𝑏⟶𝑆))
86		raleq 2728	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
87	85, 86	anbi12d 473	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑏 → ((𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
88	87	exbidv 1871	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑏 → (∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
89	84, 88	imbi12d 234	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑏 → ((𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝑏 ∈ 𝑋 → ∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
90		simpllr 534	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
91	89, 90, 78	rspcdva 2912	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → (𝑏 ∈ 𝑋 → ∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
92		feq1 5455	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (𝑔:𝑏⟶𝑆 ↔ 𝑎:𝑏⟶𝑆))
93		fveq1 5625	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑢) = (𝑎‘𝑢))
94		reseq1 4998	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑎 → (𝑔 ↾ 𝑢) = (𝑎 ↾ 𝑢))
95	94	fveq2d 5630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → (𝐺‘(𝑔 ↾ 𝑢)) = (𝐺‘(𝑎 ↾ 𝑢)))
96	93, 95	eqeq12d 2244	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑎 → ((𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
97	96	ralbidv 2530	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
98	92, 97	anbi12d 473	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → ((𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)))))
99	98	cbvexv 1965	. . . . . . . . . . . . 13 ⊢ (∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
100		fveq2 5626	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑐 → (𝑎‘𝑢) = (𝑎‘𝑐))
101		reseq2 4999	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑐 → (𝑎 ↾ 𝑢) = (𝑎 ↾ 𝑐))
102	101	fveq2d 5630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑐 → (𝐺‘(𝑎 ↾ 𝑢)) = (𝐺‘(𝑎 ↾ 𝑐)))
103	100, 102	eqeq12d 2244	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑐 → ((𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)) ↔ (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
104	103	cbvralv 2765	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)) ↔ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))
105	104	anbi2i 457	. . . . . . . . . . . . . 14 ⊢ ((𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))) ↔ (𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
106	105	exbii 1651	. . . . . . . . . . . . 13 ⊢ (∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
107	99, 106	bitri 184	. . . . . . . . . . . 12 ⊢ (∃𝑔(𝑔:𝑏⟶𝑆 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
108	91, 107	imbitrdi 161	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → (𝑏 ∈ 𝑋 → ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))))
109	83, 108	mpd 13	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
110	109	ralrimiva 2603	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∀𝑏 ∈ 𝑧 ∃𝑎(𝑎:𝑏⟶𝑆 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
111	18, 20, 21, 35, 45, 72, 76, 77, 110	tfrcllemex 6504	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∃ℎ(ℎ:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))))
112		feq1 5455	. . . . . . . . . 10 ⊢ (ℎ = 𝑔 → (ℎ:𝑧⟶𝑆 ↔ 𝑔:𝑧⟶𝑆))
113		fveq1 5625	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (ℎ‘𝑢) = (𝑔‘𝑢))
114		reseq1 4998	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → (ℎ ↾ 𝑢) = (𝑔 ↾ 𝑢))
115	114	fveq2d 5630	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (𝐺‘(ℎ ↾ 𝑢)) = (𝐺‘(𝑔 ↾ 𝑢)))
116	113, 115	eqeq12d 2244	. . . . . . . . . . 11 ⊢ (ℎ = 𝑔 → ((ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢)) ↔ (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
117	116	ralbidv 2530	. . . . . . . . . 10 ⊢ (ℎ = 𝑔 → (∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
118	112, 117	anbi12d 473	. . . . . . . . 9 ⊢ (ℎ = 𝑔 → ((ℎ:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))) ↔ (𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
119	118	cbvexv 1965	. . . . . . . 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 2536	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ∀𝑤 ∈ 𝑧 (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
126		r19.21v 2607	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
127	125, 126	bitri 184	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
128		impexp 263	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
129	123, 127, 128	3imtr4g 205	. . 3 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔:𝑤⟶𝑆 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → ((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
130	10, 17, 129	tfis3 4677	. 2 ⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
131	3, 130	mpcom 36	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002  ∀wal 1393   = wceq 1395  ∃wex 1538   ∈ wcel 2200  {cab 2215  ∀wral 2508  ∃wrex 2509   ∪ cun 3195  {csn 3666  ⟨cop 3669  ∪ cuni 3887  Ord word 4452  Oncon0 4453  suc csuc 4455   ↾ cres 4720  Fun wfun 5311  ⟶wf 5313  ‘cfv 5317  recscrecs 6448

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4198  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-setind 4628

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-iun 3966  df-br 4083  df-opab 4145  df-mpt 4146  df-tr 4182  df-id 4383  df-iord 4456  df-on 4458  df-suc 4461  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-res 4730  df-ima 4731  df-iota 5277  df-fun 5319  df-fn 5320  df-f 5321  df-f1 5322  df-fo 5323  df-f1o 5324  df-fv 5325  df-recs 6449

This theorem is referenced by:  tfrcllemres  6506