Theorem tfr1onlemaccex 6043

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 4173	. . 3 ⊢ ((Ord 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ On)
3	1, 2	sylan 277	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ On)
4		eleq1 2145	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝑋 ↔ 𝑤 ∈ 𝑋))
5	4	anbi2d 452	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝜑 ∧ 𝑧 ∈ 𝑋) ↔ (𝜑 ∧ 𝑤 ∈ 𝑋)))
6		fneq2 5054	. . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑔 Fn 𝑧 ↔ 𝑔 Fn 𝑤))
7		raleq 2555	. . . . . 6 ⊢ (𝑧 = 𝑤 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
8	6, 7	anbi12d 457	. . . . 5 ⊢ (𝑧 = 𝑤 → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
9	8	exbidv 1748	. . . 4 ⊢ (𝑧 = 𝑤 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
10	5, 9	imbi12d 232	. . 3 ⊢ (𝑧 = 𝑤 → (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
11		eleq1 2145	. . . . 5 ⊢ (𝑧 = 𝐶 → (𝑧 ∈ 𝑋 ↔ 𝐶 ∈ 𝑋))
12	11	anbi2d 452	. . . 4 ⊢ (𝑧 = 𝐶 → ((𝜑 ∧ 𝑧 ∈ 𝑋) ↔ (𝜑 ∧ 𝐶 ∈ 𝑋)))
13		fneq2 5054	. . . . . 6 ⊢ (𝑧 = 𝐶 → (𝑔 Fn 𝑧 ↔ 𝑔 Fn 𝐶))
14		raleq 2555	. . . . . 6 ⊢ (𝑧 = 𝐶 → (∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
15	13, 14	anbi12d 457	. . . . 5 ⊢ (𝑧 = 𝐶 → ((𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
16	15	exbidv 1748	. . . 4 ⊢ (𝑧 = 𝐶 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
17	12, 16	imbi12d 232	. . 3 ⊢ (𝑧 = 𝐶 → (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
18		tfr1on.f	. . . . . . . . 9 ⊢ 𝐹 = recs(𝐺)
19		tfr1on.g	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐺)
20	19	ad3antrrr 476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → Fun 𝐺)
21	1	ad3antrrr 476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → Ord 𝑋)
22		tfr1on.ex	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)
23	22	3expia 1141	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V))
24	23	alrimiv 1797	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V))
25		fneq1 5053	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → (𝑓 Fn 𝑥 ↔ ℎ Fn 𝑥))
26		fveq2 5251	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = ℎ → (𝐺‘𝑓) = (𝐺‘ℎ))
27	26	eleq1d 2151	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → ((𝐺‘𝑓) ∈ V ↔ (𝐺‘ℎ) ∈ V))
28	25, 27	imbi12d 232	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → ((𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V) ↔ (ℎ Fn 𝑥 → (𝐺‘ℎ) ∈ V)))
29	28	cbvalv 1837	. . . . . . . . . . . . . . 15 ⊢ (∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V) ↔ ∀ℎ(ℎ Fn 𝑥 → (𝐺‘ℎ) ∈ V))
30	24, 29	sylib 120	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀ℎ(ℎ Fn 𝑥 → (𝐺‘ℎ) ∈ V))
31	30	19.21bi 1491	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (ℎ Fn 𝑥 → (𝐺‘ℎ) ∈ V))
32	31	3impia 1136	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ ℎ Fn 𝑥) → (𝐺‘ℎ) ∈ V)
33	32	3adant1r 1163	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝑥 ∈ 𝑋 ∧ ℎ Fn 𝑥) → (𝐺‘ℎ) ∈ V)
34	33	3adant1r 1163	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑥 ∈ 𝑋 ∧ ℎ Fn 𝑥) → (𝐺‘ℎ) ∈ V)
35	34	3adant1r 1163	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝑋 ∧ ℎ Fn 𝑥) → (𝐺‘ℎ) ∈ V)
36		tfr1onlemsucfn.1	. . . . . . . . . 10 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}
37		fveq1 5250	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝑓‘𝑦) = (ℎ‘𝑦))
38		reseq1 4663	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → (𝑓 ↾ 𝑦) = (ℎ ↾ 𝑦))
39	38	fveq2d 5255	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝐺‘(𝑓 ↾ 𝑦)) = (𝐺‘(ℎ ↾ 𝑦)))
40	37, 39	eqeq12d 2097	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ℎ → ((𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦))))
41	40	ralbidv 2374	. . . . . . . . . . . . 13 ⊢ (𝑓 = ℎ → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦))))
42	25, 41	anbi12d 457	. . . . . . . . . . . 12 ⊢ (𝑓 = ℎ → ((𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ (ℎ Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))))
43	42	rexbidv 2375	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ 𝑋 (ℎ Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))))
44	43	cbvabv 2206	. . . . . . . . . 10 ⊢ {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} = {ℎ ∣ ∃𝑥 ∈ 𝑋 (ℎ Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))}
45	36, 44	eqtri 2103	. . . . . . . . 9 ⊢ 𝐴 = {ℎ ∣ ∃𝑥 ∈ 𝑋 (ℎ Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (ℎ‘𝑦) = (𝐺‘(ℎ ↾ 𝑦)))}
46		fneq1 5053	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑟 Fn 𝑡 ↔ 𝑎 Fn 𝑡))
47		eleq1 2145	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑟 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
48		id 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑎 → 𝑟 = 𝑎)
49		fveq2 5251	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑎 → (𝐺‘𝑟) = (𝐺‘𝑎))
50	49	opeq2d 3603	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑎 → ⟨𝑡, (𝐺‘𝑟)⟩ = ⟨𝑡, (𝐺‘𝑎)⟩)
51	50	sneqd 3435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑎 → {⟨𝑡, (𝐺‘𝑟)⟩} = {⟨𝑡, (𝐺‘𝑎)⟩})
52	48, 51	uneq12d 3139	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑎 → (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}) = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}))
53	52	eqeq2d 2094	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → (𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
54	46, 47, 53	3anbi123d 1244	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑎 → ((𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ (𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}))))
55	54	cbvexv 1838	. . . . . . . . . . . . 13 ⊢ (∃𝑟(𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
56	55	rexbii 2379	. . . . . . . . . . . 12 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑟(𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑡 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})))
57		fneq2 5054	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (𝑎 Fn 𝑡 ↔ 𝑎 Fn 𝑏))
58		opeq1 3596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑏 → ⟨𝑡, (𝐺‘𝑎)⟩ = ⟨𝑏, (𝐺‘𝑎)⟩)
59	58	sneqd 3435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑏 → {⟨𝑡, (𝐺‘𝑎)⟩} = {⟨𝑏, (𝐺‘𝑎)⟩})
60	59	uneq2d 3138	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑏 → (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}) = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))
61	60	eqeq2d 2094	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑏 → (𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
62	57, 61	3anbi13d 1246	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑏 → ((𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ (𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
63	62	exbidv 1748	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑏 → (∃𝑎(𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
64	63	cbvrexv 2584	. . . . . . . . . . . 12 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑡 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺‘𝑎)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
65	56, 64	bitri 182	. . . . . . . . . . 11 ⊢ (∃𝑡 ∈ 𝑧 ∃𝑟(𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
66	65	abbii 2198	. . . . . . . . . 10 ⊢ {𝑠 ∣ ∃𝑡 ∈ 𝑧 ∃𝑟(𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}))} = {𝑠 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
67		eqeq1 2089	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑑 → (𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}) ↔ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})))
68	67	3anbi3d 1250	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑑 → ((𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ (𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
69	68	exbidv 1748	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑑 → (∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
70	69	rexbidv 2375	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑑 → (∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩})) ↔ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))))
71	70	cbvabv 2206	. . . . . . . . . 10 ⊢ {𝑠 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))} = {𝑑 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
72	66, 71	eqtri 2103	. . . . . . . . 9 ⊢ {𝑠 ∣ ∃𝑡 ∈ 𝑧 ∃𝑟(𝑟 Fn 𝑡 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺‘𝑟)⟩}))} = {𝑑 ∣ ∃𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ 𝑎 ∈ 𝐴 ∧ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺‘𝑎)⟩}))}
73		tfr1onlemaccex.u	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
74	73	adantlr 461	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
75	74	adantlr 461	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
76	75	adantlr 461	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
77		simpr 108	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋)
78		simpr 108	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑏 ∈ 𝑧)
79		simplr 497	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑧 ∈ 𝑋)
80		ordtr1 4178	. . . . . . . . . . . . . 14 ⊢ (Ord 𝑋 → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
81	1, 80	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
82	81	ad4antr 478	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ((𝑏 ∈ 𝑧 ∧ 𝑧 ∈ 𝑋) → 𝑏 ∈ 𝑋))
83	78, 79, 82	mp2and 424	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → 𝑏 ∈ 𝑋)
84		eleq1 2145	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑏 → (𝑤 ∈ 𝑋 ↔ 𝑏 ∈ 𝑋))
85		fneq2 5054	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (𝑔 Fn 𝑤 ↔ 𝑔 Fn 𝑏))
86		raleq 2555	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑏 → (∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
87	85, 86	anbi12d 457	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑏 → ((𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
88	87	exbidv 1748	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑏 → (∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
89	84, 88	imbi12d 232	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑏 → ((𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝑏 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
90		simpllr 501	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
91	89, 90, 78	rspcdva 2717	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → (𝑏 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
92		fneq1 5053	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (𝑔 Fn 𝑏 ↔ 𝑎 Fn 𝑏))
93		fveq1 5250	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑢) = (𝑎‘𝑢))
94		reseq1 4663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑎 → (𝑔 ↾ 𝑢) = (𝑎 ↾ 𝑢))
95	94	fveq2d 5255	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑎 → (𝐺‘(𝑔 ↾ 𝑢)) = (𝐺‘(𝑎 ↾ 𝑢)))
96	93, 95	eqeq12d 2097	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑎 → ((𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
97	96	ralbidv 2374	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
98	92, 97	anbi12d 457	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → ((𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ (𝑎 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)))))
99	98	cbvexv 1838	. . . . . . . . . . . . 13 ⊢ (∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))))
100		fveq2 5251	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑐 → (𝑎‘𝑢) = (𝑎‘𝑐))
101		reseq2 4664	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑐 → (𝑎 ↾ 𝑢) = (𝑎 ↾ 𝑐))
102	101	fveq2d 5255	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑐 → (𝐺‘(𝑎 ↾ 𝑢)) = (𝐺‘(𝑎 ↾ 𝑐)))
103	100, 102	eqeq12d 2097	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑐 → ((𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)) ↔ (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
104	103	cbvralv 2583	. . . . . . . . . . . . . . 15 ⊢ (∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢)) ↔ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))
105	104	anbi2i 445	. . . . . . . . . . . . . 14 ⊢ ((𝑎 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))) ↔ (𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
106	105	exbii 1537	. . . . . . . . . . . . 13 ⊢ (∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑎‘𝑢) = (𝐺‘(𝑎 ↾ 𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
107	99, 106	bitri 182	. . . . . . . . . . . 12 ⊢ (∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢 ∈ 𝑏 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
108	91, 107	syl6ib 159	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → (𝑏 ∈ 𝑋 → ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐)))))
109	83, 108	mpd 13	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ 𝑧) → ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
110	109	ralrimiva 2440	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∀𝑏 ∈ 𝑧 ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐 ∈ 𝑏 (𝑎‘𝑐) = (𝐺‘(𝑎 ↾ 𝑐))))
111	18, 20, 21, 35, 45, 72, 76, 77, 110	tfr1onlemex 6042	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∃ℎ(ℎ Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))))
112		fneq1 5053	. . . . . . . . . 10 ⊢ (ℎ = 𝑔 → (ℎ Fn 𝑧 ↔ 𝑔 Fn 𝑧))
113		fveq1 5250	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (ℎ‘𝑢) = (𝑔‘𝑢))
114		reseq1 4663	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑔 → (ℎ ↾ 𝑢) = (𝑔 ↾ 𝑢))
115	114	fveq2d 5255	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑔 → (𝐺‘(ℎ ↾ 𝑢)) = (𝐺‘(𝑔 ↾ 𝑢)))
116	113, 115	eqeq12d 2097	. . . . . . . . . . 11 ⊢ (ℎ = 𝑔 → ((ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢)) ↔ (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
117	116	ralbidv 2374	. . . . . . . . . 10 ⊢ (ℎ = 𝑔 → (∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
118	112, 117	anbi12d 457	. . . . . . . . 9 ⊢ (ℎ = 𝑔 → ((ℎ Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))) ↔ (𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
119	118	cbvexv 1838	. . . . . . . 8 ⊢ (∃ℎ(ℎ Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (ℎ‘𝑢) = (𝐺‘(ℎ ↾ 𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
120	111, 119	sylib 120	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
121	120	exp31 356	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
122	121	expcom 114	. . . . 5 ⊢ (𝑧 ∈ On → (𝜑 → (∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))))
123	122	a2d 26	. . . 4 ⊢ (𝑧 ∈ On → ((𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → (𝜑 → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))))
124		impexp 259	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
125	124	ralbii 2378	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ ∀𝑤 ∈ 𝑧 (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
126		r19.21v 2444	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 (𝜑 → (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
127	125, 126	bitri 182	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → ∀𝑤 ∈ 𝑧 (𝑤 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
128		impexp 259	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) ↔ (𝜑 → (𝑧 ∈ 𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
129	123, 127, 128	3imtr4g 203	. . 3 ⊢ (𝑧 ∈ On → (∀𝑤 ∈ 𝑧 ((𝜑 ∧ 𝑤 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) → ((𝜑 ∧ 𝑧 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))))
130	10, 17, 129	tfis3 4363	. 2 ⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
131	3, 130	mpcom 36	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920  ∀wal 1283   = wceq 1285  ∃wex 1422   ∈ wcel 1434  {cab 2069  ∀wral 2353  ∃wrex 2354  Vcvv 2612   ∪ cun 2982  {csn 3422  ⟨cop 3425  ∪ cuni 3627  Ord word 4152  Oncon0 4153  suc csuc 4155   ↾ cres 4401  Fun wfun 4961   Fn wfn 4962  ‘cfv 4967  recscrecs 5999

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3919  ax-sep 3922  ax-pow 3974  ax-pr 3999  ax-un 4223  ax-setind 4315

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2614  df-sbc 2827  df-csb 2920  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-iun 3706  df-br 3812  df-opab 3866  df-mpt 3867  df-tr 3902  df-id 4083  df-iord 4156  df-on 4158  df-suc 4161  df-xp 4405  df-rel 4406  df-cnv 4407  df-co 4408  df-dm 4409  df-rn 4410  df-res 4411  df-ima 4412  df-iota 4932  df-fun 4969  df-fn 4970  df-f 4971  df-f1 4972  df-fo 4973  df-f1o 4974  df-fv 4975  df-recs 6000

This theorem is referenced by:  tfr1onlemres  6044