Theorem tfr1onlemsucaccv 6572

Description: Lemma for tfr1on 6581. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 12-Mar-2022.)

Hypotheses

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

Assertion

Ref	Expression
tfr1onlemsucaccv	⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ 𝐴)

Distinct variable groups:   𝑓,𝐺,𝑥,𝑦   𝑓,𝑋,𝑥   𝑓,𝑔,𝑥,𝑦   𝜑,𝑓,𝑥   𝑧,𝑓,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑦,𝑧,𝑔)   𝐴(𝑥,𝑦,𝑧,𝑓,𝑔)   𝐹(𝑥,𝑦,𝑧,𝑓,𝑔)   𝐺(𝑧,𝑔)   𝑋(𝑦,𝑧,𝑔)   𝑌(𝑥,𝑦,𝑧,𝑓,𝑔)

Proof of Theorem tfr1onlemsucaccv

Dummy variables 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		suceq 4523	. . . . 5 ⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
2	1	eleq1d 2301	. . . 4 ⊢ (𝑥 = 𝑧 → (suc 𝑥 ∈ 𝑋 ↔ suc 𝑧 ∈ 𝑋))
3		tfr1onlemsucaccv.u	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
4	3	ralrimiva 2615	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ∪ 𝑋 suc 𝑥 ∈ 𝑋)
5		tfr1onlemsucaccv.zy	. . . . 5 ⊢ (𝜑 → 𝑧 ∈ 𝑌)
6		tfr1onlemsucaccv.yx	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑋)
7		elunii 3919	. . . . 5 ⊢ ((𝑧 ∈ 𝑌 ∧ 𝑌 ∈ 𝑋) → 𝑧 ∈ ∪ 𝑋)
8	5, 6, 7	syl2anc 411	. . . 4 ⊢ (𝜑 → 𝑧 ∈ ∪ 𝑋)
9	2, 4, 8	rspcdva 2926	. . 3 ⊢ (𝜑 → suc 𝑧 ∈ 𝑋)
10		tfr1on.f	. . . 4 ⊢ 𝐹 = recs(𝐺)
11		tfr1on.g	. . . 4 ⊢ (𝜑 → Fun 𝐺)
12		tfr1on.x	. . . 4 ⊢ (𝜑 → Ord 𝑋)
13		tfr1on.ex	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V)
14		tfr1onlemsucfn.1	. . . 4 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))}
15	5, 6	jca 306	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ 𝑌 ∧ 𝑌 ∈ 𝑋))
16		ordtr1 4509	. . . . 5 ⊢ (Ord 𝑋 → ((𝑧 ∈ 𝑌 ∧ 𝑌 ∈ 𝑋) → 𝑧 ∈ 𝑋))
17	12, 15, 16	sylc 62	. . . 4 ⊢ (𝜑 → 𝑧 ∈ 𝑋)
18		tfr1onlemsucaccv.gfn	. . . 4 ⊢ (𝜑 → 𝑔 Fn 𝑧)
19		tfr1onlemsucaccv.gacc	. . . 4 ⊢ (𝜑 → 𝑔 ∈ 𝐴)
20	10, 11, 12, 13, 14, 17, 18, 19	tfr1onlemsucfn 6571	. . 3 ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn suc 𝑧)
21		vex 2816	. . . . . 6 ⊢ 𝑢 ∈ V
22	21	elsuc 4527	. . . . 5 ⊢ (𝑢 ∈ suc 𝑧 ↔ (𝑢 ∈ 𝑧 ∨ 𝑢 = 𝑧))
23		vex 2816	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
24	14	tfr1onlem3ag 6568	. . . . . . . . . . 11 ⊢ (𝑔 ∈ V → (𝑔 ∈ 𝐴 ↔ ∃𝑣 ∈ 𝑋 (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
25	23, 24	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑣 ∈ 𝑋 (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
26	19, 25	sylib 122	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑣 ∈ 𝑋 (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
27		simprrr 542	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))
28		simprrl 541	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → 𝑔 Fn 𝑣)
29	18	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → 𝑔 Fn 𝑧)
30		fndmu 5459	. . . . . . . . . . . 12 ⊢ ((𝑔 Fn 𝑣 ∧ 𝑔 Fn 𝑧) → 𝑣 = 𝑧)
31	28, 29, 30	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → 𝑣 = 𝑧)
32	31	raleqdv 2747	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → (∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
33	27, 32	mpbid 147	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))
34	26, 33	rexlimddv 2665	. . . . . . . 8 ⊢ (𝜑 → ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))
35	34	r19.21bi 2630	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))
36		ordelon 4504	. . . . . . . . . . . . 13 ⊢ ((Ord 𝑋 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ On)
37	12, 17, 36	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑧 ∈ On)
38		onelon 4505	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ On ∧ 𝑢 ∈ 𝑧) → 𝑢 ∈ On)
39	37, 38	sylan 283	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → 𝑢 ∈ On)
40		eloni 4496	. . . . . . . . . . 11 ⊢ (𝑢 ∈ On → Ord 𝑢)
41		ordirr 4664	. . . . . . . . . . 11 ⊢ (Ord 𝑢 → ¬ 𝑢 ∈ 𝑢)
42	39, 40, 41	3syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → ¬ 𝑢 ∈ 𝑢)
43		elequ2 2208	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑢 → (𝑢 ∈ 𝑧 ↔ 𝑢 ∈ 𝑢))
44	43	biimpcd 159	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝑧 → (𝑧 = 𝑢 → 𝑢 ∈ 𝑢))
45	44	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → (𝑧 = 𝑢 → 𝑢 ∈ 𝑢))
46	42, 45	mtod 669	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → ¬ 𝑧 = 𝑢)
47	46	neqned 2419	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → 𝑧 ≠ 𝑢)
48		fvunsng 5878	. . . . . . . 8 ⊢ ((𝑢 ∈ V ∧ 𝑧 ≠ 𝑢) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝑔‘𝑢))
49	21, 47, 48	sylancr 414	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝑔‘𝑢))
50		eloni 4496	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ On → Ord 𝑧)
51	37, 50	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → Ord 𝑧)
52		ordelss 4500	. . . . . . . . . . 11 ⊢ ((Ord 𝑧 ∧ 𝑢 ∈ 𝑧) → 𝑢 ⊆ 𝑧)
53	51, 52	sylan 283	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → 𝑢 ⊆ 𝑧)
54		resabs1 5067	. . . . . . . . . 10 ⊢ (𝑢 ⊆ 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))
55	53, 54	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))
56		ordirr 4664	. . . . . . . . . . . . 13 ⊢ (Ord 𝑧 → ¬ 𝑧 ∈ 𝑧)
57	51, 56	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑧 ∈ 𝑧)
58		fsnunres 5886	. . . . . . . . . . . 12 ⊢ ((𝑔 Fn 𝑧 ∧ ¬ 𝑧 ∈ 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) = 𝑔)
59	18, 57, 58	syl2anc 411	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) = 𝑔)
60	59	reseq1d 5037	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔 ↾ 𝑢))
61	60	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔 ↾ 𝑢))
62	55, 61	eqtr3d 2267	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢) = (𝑔 ↾ 𝑢))
63	62	fveq2d 5674	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)) = (𝐺‘(𝑔 ↾ 𝑢)))
64	35, 49, 63	3eqtr4d 2275	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))
65		fneq2 5445	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑓 Fn 𝑥 ↔ 𝑓 Fn 𝑧))
66	65	imbi1d 231	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V) ↔ (𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V)))
67	66	albidv 1873	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V) ↔ ∀𝑓(𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V)))
68	13	3expia 1232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V))
69	68	alrimiv 1923	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V))
70	69	ralrimiva 2615	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V))
71	67, 70, 17	rspcdva 2926	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑓(𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V))
72		fneq1 5444	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 Fn 𝑧 ↔ 𝑔 Fn 𝑧))
73		fveq2 5670	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝐺‘𝑓) = (𝐺‘𝑔))
74	73	eleq1d 2301	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝐺‘𝑓) ∈ V ↔ (𝐺‘𝑔) ∈ V))
75	72, 74	imbi12d 234	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V) ↔ (𝑔 Fn 𝑧 → (𝐺‘𝑔) ∈ V)))
76	75	spv 1909	. . . . . . . . . 10 ⊢ (∀𝑓(𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V) → (𝑔 Fn 𝑧 → (𝐺‘𝑔) ∈ V))
77	71, 18, 76	sylc 62	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝑔) ∈ V)
78		fndm 5455	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
79	18, 78	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → dom 𝑔 = 𝑧)
80	57, 79	neleqtrrd 2331	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝑧 ∈ dom 𝑔)
81		fsnunfv 5885	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑌 ∧ (𝐺‘𝑔) ∈ V ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑧) = (𝐺‘𝑔))
82	5, 77, 80, 81	syl3anc 1274	. . . . . . . 8 ⊢ (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑧) = (𝐺‘𝑔))
83	82	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑧) = (𝐺‘𝑔))
84		simpr 110	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → 𝑢 = 𝑧)
85	84	fveq2d 5674	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑧))
86		reseq2 5033	. . . . . . . . 9 ⊢ (𝑢 = 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧))
87	86, 59	sylan9eqr 2287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢) = 𝑔)
88	87	fveq2d 5674	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)) = (𝐺‘𝑔))
89	83, 85, 88	3eqtr4d 2275	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))
90	64, 89	jaodan 805	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑧 ∨ 𝑢 = 𝑧)) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))
91	22, 90	sylan2b 287	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ suc 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))
92	91	ralrimiva 2615	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))
93		fneq2 5445	. . . . 5 ⊢ (𝑤 = suc 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ↔ (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn suc 𝑧))
94		raleq 2741	. . . . 5 ⊢ (𝑤 = suc 𝑧 → (∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)) ↔ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))))
95	93, 94	anbi12d 473	. . . 4 ⊢ (𝑤 = suc 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))))
96	95	rspcev 2921	. . 3 ⊢ ((suc 𝑧 ∈ 𝑋 ∧ ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))) → ∃𝑤 ∈ 𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))))
97	9, 20, 92, 96	syl12anc 1272	. 2 ⊢ (𝜑 → ∃𝑤 ∈ 𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))))
98		vex 2816	. . . . . 6 ⊢ 𝑧 ∈ V
99		opexg 4344	. . . . . 6 ⊢ ((𝑧 ∈ V ∧ (𝐺‘𝑔) ∈ V) → ⟨𝑧, (𝐺‘𝑔)⟩ ∈ V)
100	98, 77, 99	sylancr 414	. . . . 5 ⊢ (𝜑 → ⟨𝑧, (𝐺‘𝑔)⟩ ∈ V)
101		snexg 4297	. . . . 5 ⊢ (⟨𝑧, (𝐺‘𝑔)⟩ ∈ V → {⟨𝑧, (𝐺‘𝑔)⟩} ∈ V)
102	100, 101	syl 14	. . . 4 ⊢ (𝜑 → {⟨𝑧, (𝐺‘𝑔)⟩} ∈ V)
103		unexg 4564	. . . 4 ⊢ ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺‘𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ V)
104	23, 102, 103	sylancr 414	. . 3 ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ V)
105	14	tfr1onlem3ag 6568	. . 3 ⊢ ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ V → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤 ∈ 𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))))
106	104, 105	syl 14	. 2 ⊢ (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤 ∈ 𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))))
107	97, 106	mpbird 167	1 ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 716   ∧ w3a 1005  ∀wal 1396   = wceq 1398   ∈ wcel 2203  {cab 2218   ≠ wne 2412  ∀wral 2520  ∃wrex 2521  Vcvv 2813   ∪ cun 3209   ⊆ wss 3211  {csn 3689  ⟨cop 3692  ∪ cuni 3914  Ord word 4483  Oncon0 4484  suc csuc 4486  dom cdm 4749   ↾ cres 4751  Fun wfun 5346   Fn wfn 5347  ‘cfv 5352  recscrecs 6535

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-ral 2525  df-rex 2526  df-v 2815  df-sbc 3043  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-tr 4209  df-id 4414  df-iord 4487  df-on 4489  df-suc 4492  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-res 4761  df-iota 5312  df-fun 5354  df-fn 5355  df-fv 5360

This theorem is referenced by:  tfr1onlembacc  6573  tfr1onlemres  6580