Theorem tfr1onlemsucaccv 6309

Description: Lemma for tfr1on 6318. 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 4380	. . . . 5 ⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
2	1	eleq1d 2235	. . . 4 ⊢ (𝑥 = 𝑧 → (suc 𝑥 ∈ 𝑋 ↔ suc 𝑧 ∈ 𝑋))
3		tfr1onlemsucaccv.u	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋)
4	3	ralrimiva 2539	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ ∪ 𝑋 suc 𝑥 ∈ 𝑋)
5		tfr1onlemsucaccv.zy	. . . . 5 ⊢ (𝜑 → 𝑧 ∈ 𝑌)
6		tfr1onlemsucaccv.yx	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑋)
7		elunii 3794	. . . . 5 ⊢ ((𝑧 ∈ 𝑌 ∧ 𝑌 ∈ 𝑋) → 𝑧 ∈ ∪ 𝑋)
8	5, 6, 7	syl2anc 409	. . . 4 ⊢ (𝜑 → 𝑧 ∈ ∪ 𝑋)
9	2, 4, 8	rspcdva 2835	. . 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 304	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ 𝑌 ∧ 𝑌 ∈ 𝑋))
16		ordtr1 4366	. . . . 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 6308	. . 3 ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn suc 𝑧)
21		vex 2729	. . . . . 6 ⊢ 𝑢 ∈ V
22	21	elsuc 4384	. . . . 5 ⊢ (𝑢 ∈ suc 𝑧 ↔ (𝑢 ∈ 𝑧 ∨ 𝑢 = 𝑧))
23		vex 2729	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
24	14	tfr1onlem3ag 6305	. . . . . . . . . . 11 ⊢ (𝑔 ∈ V → (𝑔 ∈ 𝐴 ↔ ∃𝑣 ∈ 𝑋 (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))))
25	23, 24	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑣 ∈ 𝑋 (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
26	19, 25	sylib 121	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑣 ∈ 𝑋 (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
27		simprrr 530	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))
28		simprrl 529	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → 𝑔 Fn 𝑣)
29	18	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → 𝑔 Fn 𝑧)
30		fndmu 5289	. . . . . . . . . . . 12 ⊢ ((𝑔 Fn 𝑣 ∧ 𝑔 Fn 𝑧) → 𝑣 = 𝑧)
31	28, 29, 30	syl2anc 409	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → 𝑣 = 𝑧)
32	31	raleqdv 2667	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → (∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)) ↔ ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))
33	27, 32	mpbid 146	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢 ∈ 𝑣 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢))))) → ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))
34	26, 33	rexlimddv 2588	. . . . . . . 8 ⊢ (𝜑 → ∀𝑢 ∈ 𝑧 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))
35	34	r19.21bi 2554	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))
36		ordelon 4361	. . . . . . . . . . . . 13 ⊢ ((Ord 𝑋 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ On)
37	12, 17, 36	syl2anc 409	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑧 ∈ On)
38		onelon 4362	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ On ∧ 𝑢 ∈ 𝑧) → 𝑢 ∈ On)
39	37, 38	sylan 281	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → 𝑢 ∈ On)
40		eloni 4353	. . . . . . . . . . 11 ⊢ (𝑢 ∈ On → Ord 𝑢)
41		ordirr 4519	. . . . . . . . . . 11 ⊢ (Ord 𝑢 → ¬ 𝑢 ∈ 𝑢)
42	39, 40, 41	3syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → ¬ 𝑢 ∈ 𝑢)
43		elequ2 2141	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑢 → (𝑢 ∈ 𝑧 ↔ 𝑢 ∈ 𝑢))
44	43	biimpcd 158	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝑧 → (𝑧 = 𝑢 → 𝑢 ∈ 𝑢))
45	44	adantl 275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → (𝑧 = 𝑢 → 𝑢 ∈ 𝑢))
46	42, 45	mtod 653	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → ¬ 𝑧 = 𝑢)
47	46	neqned 2343	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → 𝑧 ≠ 𝑢)
48		fvunsng 5679	. . . . . . . 8 ⊢ ((𝑢 ∈ V ∧ 𝑧 ≠ 𝑢) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝑔‘𝑢))
49	21, 47, 48	sylancr 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝑔‘𝑢))
50		eloni 4353	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ On → Ord 𝑧)
51	37, 50	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → Ord 𝑧)
52		ordelss 4357	. . . . . . . . . . 11 ⊢ ((Ord 𝑧 ∧ 𝑢 ∈ 𝑧) → 𝑢 ⊆ 𝑧)
53	51, 52	sylan 281	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → 𝑢 ⊆ 𝑧)
54		resabs1 4913	. . . . . . . . . 10 ⊢ (𝑢 ⊆ 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))
55	53, 54	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))
56		ordirr 4519	. . . . . . . . . . . . 13 ⊢ (Ord 𝑧 → ¬ 𝑧 ∈ 𝑧)
57	51, 56	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑧 ∈ 𝑧)
58		fsnunres 5687	. . . . . . . . . . . 12 ⊢ ((𝑔 Fn 𝑧 ∧ ¬ 𝑧 ∈ 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) = 𝑔)
59	18, 57, 58	syl2anc 409	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) = 𝑔)
60	59	reseq1d 4883	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔 ↾ 𝑢))
61	60	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔 ↾ 𝑢))
62	55, 61	eqtr3d 2200	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢) = (𝑔 ↾ 𝑢))
63	62	fveq2d 5490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)) = (𝐺‘(𝑔 ↾ 𝑢)))
64	35, 49, 63	3eqtr4d 2208	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))
65		fneq2 5277	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑓 Fn 𝑥 ↔ 𝑓 Fn 𝑧))
66	65	imbi1d 230	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V) ↔ (𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V)))
67	66	albidv 1812	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V) ↔ ∀𝑓(𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V)))
68	13	3expia 1195	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V))
69	68	alrimiv 1862	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V))
70	69	ralrimiva 2539	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑓(𝑓 Fn 𝑥 → (𝐺‘𝑓) ∈ V))
71	67, 70, 17	rspcdva 2835	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑓(𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V))
72		fneq1 5276	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓 Fn 𝑧 ↔ 𝑔 Fn 𝑧))
73		fveq2 5486	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝐺‘𝑓) = (𝐺‘𝑔))
74	73	eleq1d 2235	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝐺‘𝑓) ∈ V ↔ (𝐺‘𝑔) ∈ V))
75	72, 74	imbi12d 233	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V) ↔ (𝑔 Fn 𝑧 → (𝐺‘𝑔) ∈ V)))
76	75	spv 1848	. . . . . . . . . 10 ⊢ (∀𝑓(𝑓 Fn 𝑧 → (𝐺‘𝑓) ∈ V) → (𝑔 Fn 𝑧 → (𝐺‘𝑔) ∈ V))
77	71, 18, 76	sylc 62	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝑔) ∈ V)
78		fndm 5287	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
79	18, 78	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → dom 𝑔 = 𝑧)
80	57, 79	neleqtrrd 2265	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝑧 ∈ dom 𝑔)
81		fsnunfv 5686	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑌 ∧ (𝐺‘𝑔) ∈ V ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑧) = (𝐺‘𝑔))
82	5, 77, 80, 81	syl3anc 1228	. . . . . . . 8 ⊢ (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑧) = (𝐺‘𝑔))
83	82	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑧) = (𝐺‘𝑔))
84		simpr 109	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → 𝑢 = 𝑧)
85	84	fveq2d 5490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑧))
86		reseq2 4879	. . . . . . . . 9 ⊢ (𝑢 = 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑧))
87	86, 59	sylan9eqr 2221	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢) = 𝑔)
88	87	fveq2d 5490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)) = (𝐺‘𝑔))
89	83, 85, 88	3eqtr4d 2208	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))
90	64, 89	jaodan 787	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝑧 ∨ 𝑢 = 𝑧)) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))
91	22, 90	sylan2b 285	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ suc 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))
92	91	ralrimiva 2539	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))
93		fneq2 5277	. . . . 5 ⊢ (𝑤 = suc 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ↔ (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn suc 𝑧))
94		raleq 2661	. . . . 5 ⊢ (𝑤 = suc 𝑧 → (∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)) ↔ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))))
95	93, 94	anbi12d 465	. . . 4 ⊢ (𝑤 = suc 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))))
96	95	rspcev 2830	. . 3 ⊢ ((suc 𝑧 ∈ 𝑋 ∧ ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))) → ∃𝑤 ∈ 𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))))
97	9, 20, 92, 96	syl12anc 1226	. 2 ⊢ (𝜑 → ∃𝑤 ∈ 𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢))))
98		vex 2729	. . . . . 6 ⊢ 𝑧 ∈ V
99		opexg 4206	. . . . . 6 ⊢ ((𝑧 ∈ V ∧ (𝐺‘𝑔) ∈ V) → ⟨𝑧, (𝐺‘𝑔)⟩ ∈ V)
100	98, 77, 99	sylancr 411	. . . . 5 ⊢ (𝜑 → ⟨𝑧, (𝐺‘𝑔)⟩ ∈ V)
101		snexg 4163	. . . . 5 ⊢ (⟨𝑧, (𝐺‘𝑔)⟩ ∈ V → {⟨𝑧, (𝐺‘𝑔)⟩} ∈ V)
102	100, 101	syl 14	. . . 4 ⊢ (𝜑 → {⟨𝑧, (𝐺‘𝑔)⟩} ∈ V)
103		unexg 4421	. . . 4 ⊢ ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺‘𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ V)
104	23, 102, 103	sylancr 411	. . 3 ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ V)
105	14	tfr1onlem3ag 6305	. . 3 ⊢ ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ V → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤 ∈ 𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))))
106	104, 105	syl 14	. 2 ⊢ (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤 ∈ 𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢 ∈ 𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ↾ 𝑢)))))
107	97, 106	mpbird 166	1 ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺‘𝑔)⟩}) ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   ∧ w3a 968  ∀wal 1341   = wceq 1343   ∈ wcel 2136  {cab 2151   ≠ wne 2336  ∀wral 2444  ∃wrex 2445  Vcvv 2726   ∪ cun 3114   ⊆ wss 3116  {csn 3576  ⟨cop 3579  ∪ cuni 3789  Ord word 4340  Oncon0 4341  suc csuc 4343  dom cdm 4604   ↾ cres 4606  Fun wfun 5182   Fn wfn 5183  ‘cfv 5188  recscrecs 6272

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 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-sep 4100  ax-pow 4153  ax-pr 4187  ax-un 4411  ax-setind 4514

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ne 2337  df-ral 2449  df-rex 2450  df-v 2728  df-sbc 2952  df-dif 3118  df-un 3120  df-in 3122  df-ss 3129  df-nul 3410  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-opab 4044  df-tr 4081  df-id 4271  df-iord 4344  df-on 4346  df-suc 4349  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-res 4616  df-iota 5153  df-fun 5190  df-fn 5191  df-fv 5196

This theorem is referenced by:  tfr1onlembacc  6310  tfr1onlemres  6317