Theorem tfr1onlemaccex 6324

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, 16-Mar-2022.)

Hypotheses

Ref	Expression
tfr1on.f	⊢ 𝐹 = recs(𝐺)
tfr1on.g	⊢ (𝜑 → Fun 𝐺)
tfr1on.x	⊢ (𝜑 → Ord 𝑋)
tfr1on.ex	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)
tfr1onlemsucfn.1	⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}
tfr1onlemaccex.u	⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)

Assertion

Ref	Expression
tfr1onlemaccex	⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))

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

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

Proof of Theorem tfr1onlemaccex

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

Step	Hyp	Ref	Expression
1		tfr1on.x	. . 3 ⊢ (𝜑 → Ord 𝑋)
2		ordelon 4366	. . 3 ⊢ ((Ord 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ On)
3	1, 2	sylan 281	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ On)
4		eleq1 2233	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝑋 ↔ 𝑤 ∈ 𝑋))
5	4	anbi2d 461	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝜑 ∧ 𝑧 ∈ 𝑋) ↔ (𝜑 ∧ 𝑤 ∈ 𝑋)))
6		fneq2 5285	. . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑔 Fn 𝑧 ↔ 𝑔 Fn 𝑤))
7		raleq 2665	. . . . . 6 ⊢ (𝑧 = 𝑤 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
8	6, 7	anbi12d 470	. . . . 5 ⊢ (𝑧 = 𝑤 → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
9	8	exbidv 1818	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
10	5, 9	imbi12d 233	. . 3 ⊢ (𝑧 = 𝑤 → (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
11		eleq1 2233	. . . . 5 ⊢ (𝑧 = 𝐶 → (𝑧 ∈ 𝑋 ↔ 𝐶 ∈ 𝑋))
12	11	anbi2d 461	. . . 4 ⊢ (𝑧 = 𝐶 → ((𝜑 ∧ 𝑧 ∈ 𝑋) ↔ (𝜑 ∧ 𝐶 ∈ 𝑋)))
13		fneq2 5285	. . . . . 6 ⊢ (𝑧 = 𝐶 → (𝑔 Fn 𝑧 ↔ 𝑔 Fn 𝐶))
14		raleq 2665	. . . . . 6 ⊢ (𝑧 = 𝐶 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
15	13, 14	anbi12d 470	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
16	15	exbidv 1818	. . . 4 ⊢ (𝑧 = 𝐶 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
17	12, 16	imbi12d 233	. . 3 ⊢ (𝑧 = 𝐶 → (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
18		tfr1on.f	. . . . . . . . 9 ⊢ 𝐹 = recs(𝐺)
19		tfr1on.g	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐺)
20	19	ad3antrrr 489	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → Fun 𝐺)
21	1	ad3antrrr 489	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → Ord 𝑋)
22		tfr1on.ex	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)
23	22	3expia 1200	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V))
24	23	alrimiv 1867	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V))
25		fneq1 5284	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → (𝑓 Fn 𝑥 ↔ ℎ Fn 𝑥))
26		fveq2 5494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = ℎ → (𝐺‘𝑓) = (𝐺‘ℎ))
27	26	eleq1d 2239	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → ((𝐺‘𝑓) ∈ V ↔ (𝐺‘ℎ) ∈ V))
28	25, 27	imbi12d 233	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → ((𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V) ↔ (ℎ Fn 𝑥 → (𝐺‘ℎ) ∈ V)))
29	28	cbvalv 1910	. . . . . . . . . . . . . . 15 ⊢ (∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V) ↔ ∀ℎ(ℎ Fn 𝑥 → (𝐺‘ℎ) ∈ V))
30	24, 29	sylib 121	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀ℎ(ℎ Fn 𝑥 → (𝐺‘ℎ) ∈ V))
31	30	19.21bi 1551	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (ℎ Fn 𝑥 → (𝐺‘ℎ) ∈ V))
32	31	3impia 1195	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ℎ Fn 𝑥) → (𝐺‘ℎ) ∈ V)
33	32	3adant1r 1226	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝑥 ∈ 𝑋 ∧ ℎ Fn 𝑥) → (𝐺‘ℎ) ∈ V)
34	33	3adant1r 1226	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑥 ∈ 𝑋 ∧ ℎ Fn 𝑥) → (𝐺‘ℎ) ∈ V)
35	34	3adant1r 1226	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝑋 ∧ ℎ Fn 𝑥) → (𝐺‘ℎ) ∈ V)
36		tfr1onlemsucfn.1	. . . . . . . . . 10 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}
37		fveq1 5493	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝑓‘𝑦) = (ℎ‘𝑦))
38		reseq1 4883	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → (𝑓 ↾ 𝑦) = (ℎ ↾ 𝑦))
39	38	fveq2d 5498	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝐺‘(𝑓 ↾ 𝑦)) = (𝐺‘(ℎ ↾ 𝑦)))
40	37, 39	eqeq12d 2185	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ℎ → ((𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦))))
41	40	ralbidv 2470	. . . . . . . . . . . . 13 ⊢ (𝑓 = ℎ → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦))))
42	25, 41	anbi12d 470	. . . . . . . . . . . 12 ⊢ (𝑓 = ℎ → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ (ℎ Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))))
43	42	rexbidv 2471	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ 𝑋 (ℎ Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))))
44	43	cbvabv 2295	. . . . . . . . . 10 ⊢ {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} = {ℎ ∣ ∃𝑥 ∈ 𝑋 (ℎ Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))}
45	36, 44	eqtri 2191	. . . . . . . . 9 ⊢ 𝐴 = {ℎ ∣ ∃𝑥 ∈ 𝑋 (ℎ Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))}
46		fneq1 5284	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑟 Fn 𝑡 ↔ 𝑎 Fn 𝑡))
47		eleq1 2233	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑟 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
48		id 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑎 → 𝑟 = 𝑎)
49		fveq2 5494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑎 → (𝐺‘𝑟) = (𝐺‘𝑎))
50	49	opeq2d 3770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑎 → ⟨𝑡, (𝐺‘𝑟)⟩ = ⟨𝑡, (𝐺‘𝑎)⟩)
51	50	sneqd 3594	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑎 → {⟨𝑡, (𝐺‘𝑟)⟩} = {⟨𝑡, (𝐺‘𝑎)⟩})
52	48, 51	uneq12d 3282	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑎 → (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}) = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}))
53	52	eqeq2d 2182	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
54	46, 47, 53	3anbi123d 1307	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑎 → ((𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ (𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}))))
55	54	cbvexv 1911	. . . . . . . . . . . . 13 ⊢ (∃𝑟(𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
56	55	rexbii 2477	. . . . . . . . . . . 12 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑟(𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑡 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
57		fneq2 5285	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (𝑎 Fn 𝑡 ↔ 𝑎 Fn 𝑏))
58		opeq1 3763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑏 → ⟨𝑡, (𝐺‘𝑎)⟩ = ⟨𝑏, (𝐺‘𝑎)⟩)
59	58	sneqd 3594	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → {⟨𝑡, (𝐺‘𝑎)⟩} = {⟨𝑏, (𝐺‘𝑎)⟩})
60	59	uneq2d 3281	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}) = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))
61	60	eqeq2d 2182	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
62	57, 61	3anbi13d 1309	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → ((𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ (𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
63	62	exbidv 1818	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑏 → (∃𝑎(𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
64	63	cbvrexv 2697	. . . . . . . . . . . 12 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
65	56, 64	bitri 183	. . . . . . . . . . 11 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑟(𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
66	65	abbii 2286	. . . . . . . . . 10 ⊢ {𝑠 ∣ ∃𝑡 ∈ 𝑧 ∃𝑟(𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}))} = {𝑠 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
67		eqeq1 2177	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑑 → (𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}) ↔ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
68	67	3anbi3d 1313	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑑 → ((𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ (𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
69	68	exbidv 1818	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑑 → (∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
70	69	rexbidv 2471	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑑 → (∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
71	70	cbvabv 2295	. . . . . . . . . 10 ⊢ {𝑠 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))} = {𝑑 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
72	66, 71	eqtri 2191	. . . . . . . . 9 ⊢ {𝑠 ∣ ∃𝑡 ∈ 𝑧 ∃𝑟(𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}))} = {𝑑 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
73		tfr1onlemaccex.u	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
74	73	adantlr 474	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
75	74	adantlr 474	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
76	75	adantlr 474	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
77		simpr 109	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋)
78		simpr 109	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑏 ∈ 𝑧)
79		simplr 525	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑧 ∈ 𝑋)
80		ordtr1 4371	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑋 → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
81	1, 80	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
82	81	ad4antr 491	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
83	78, 79, 82	mp2and 431	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑏 ∈ 𝑋)
84		eleq1 2233	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑏 → (𝑤 ∈ 𝑋 ↔ 𝑏 ∈ 𝑋))
85		fneq2 5285	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝑔 Fn 𝑤 ↔ 𝑔 Fn 𝑏))
86		raleq 2665	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
87	85, 86	anbi12d 470	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑏 → ((𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
88	87	exbidv 1818	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑏 → (∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
89	84, 88	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑏 → ((𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝑏 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
90		simpllr 529	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
91	89, 90, 78	rspcdva 2839	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → (𝑏 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
92		fneq1 5284	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (𝑔 Fn 𝑏 ↔ 𝑎 Fn 𝑏))
93		fveq1 5493	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑢) = (𝑎‘𝑢))
94		reseq1 4883	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑎 → (𝑔 ↾ 𝑢) = (𝑎 ↾ 𝑢))
95	94	fveq2d 5498	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → (𝐺‘(𝑔 ↾ 𝑢)) = (𝐺‘(𝑎 ↾ 𝑢)))
96	93, 95	eqeq12d 2185	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑎 → ((𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
97	96	ralbidv 2470	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
98	92, 97	anbi12d 470	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → ((𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑎 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)))))
99	98	cbvexv 1911	. . . . . . . . . . . . 13 ⊢ (∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
100		fveq2 5494	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑐 → (𝑎‘𝑢) = (𝑎‘𝑐))
101		reseq2 4884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑐 → (𝑎 ↾ 𝑢) = (𝑎 ↾ 𝑐))
102	101	fveq2d 5498	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑐 → (𝐺‘(𝑎 ↾ 𝑢)) = (𝐺‘(𝑎 ↾ 𝑐)))
103	100, 102	eqeq12d 2185	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑐 → ((𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)) ↔ (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
104	103	cbvralv 2696	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)) ↔ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))
105	104	anbi2i 454	. . . . . . . . . . . . . 14 ⊢ ((𝑎 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))) ↔ (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
106	105	exbii 1598	. . . . . . . . . . . . 13 ⊢ (∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
107	99, 106	bitri 183	. . . . . . . . . . . 12 ⊢ (∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
108	91, 107	syl6ib 160	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → (𝑏 ∈ 𝑋 → ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))))
109	83, 108	mpd 13	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
110	109	ralrimiva 2543	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∀𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
111	18, 20, 21, 35, 45, 72, 76, 77, 110	tfr1onlemex 6323	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∃ℎ(ℎ Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))))
112		fneq1 5284	. . . . . . . . . 10 ⊢ (ℎ = 𝑔 → (ℎ Fn 𝑧 ↔ 𝑔 Fn 𝑧))
113		fveq1 5493	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (ℎ‘𝑢) = (𝑔‘𝑢))
114		reseq1 4883	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → (ℎ ↾ 𝑢) = (𝑔 ↾ 𝑢))
115	114	fveq2d 5498	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (𝐺‘(ℎ ↾ 𝑢)) = (𝐺‘(𝑔 ↾ 𝑢)))
116	113, 115	eqeq12d 2185	. . . . . . . . . . 11 ⊢ (ℎ = 𝑔 → ((ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢)) ↔ (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
117	116	ralbidv 2470	. . . . . . . . . 10 ⊢ (ℎ = 𝑔 → (∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
118	112, 117	anbi12d 470	. . . . . . . . 9 ⊢ (ℎ = 𝑔 → ((ℎ Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))) ↔ (𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
119	118	cbvexv 1911	. . . . . . . 8 ⊢ (∃ℎ(ℎ Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
120	111, 119	sylib 121	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
121	120	exp31 362	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
122	121	expcom 115	. . . . 5 ⊢ (𝑧 ∈ On → (𝜑 → (∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))))
123	122	a2d 26	. . . 4 ⊢ (𝑧 ∈ On → ((𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → (𝜑 → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))))
124		impexp 261	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
125	124	ralbii 2476	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ∀𝑤 ∈ 𝑧 (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
126		r19.21v 2547	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
127	125, 126	bitri 183	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
128		impexp 261	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
129	123, 127, 128	3imtr4g 204	. . 3 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → ((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
130	10, 17, 129	tfis3 4568	. 2 ⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
131	3, 130	mpcom 36	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 973  ∀wal 1346   = wceq 1348  ∃wex 1485   ∈ wcel 2141  {cab 2156  ∀wral 2448  ∃wrex 2449  Vcvv 2730   ∪ cun 3119  {csn 3581  ⟨cop 3584  ∪ cuni 3794  Ord word 4345  Oncon0 4346  suc csuc 4348   ↾ cres 4611  Fun wfun 5190   Fn wfn 5191  ‘cfv 5196  recscrecs 6280

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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-iord 4349  df-on 4351  df-suc 4354  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-recs 6281

This theorem is referenced by:  tfr1onlemres  6325