Theorem frrlem12 8338

Description: Lemma for well-founded recursion. Next, we calculate the value of 𝐶. (Contributed by Scott Fenton, 7-Dec-2022.)

Hypotheses

Ref	Expression
frrlem11.1	⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
frrlem11.2	⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)
frrlem11.3	⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
frrlem11.4	⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
frrlem12.5	⊢ (𝜑 → 𝑅 Fr 𝐴)
frrlem12.6	⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
frrlem12.7	⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)

Assertion

Ref	Expression
frrlem12	⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))

Distinct variable groups:   𝐴,𝑓,𝑥,𝑦,𝑧   𝑓,𝐺,𝑥,𝑦,𝑧   𝑅,𝑓,𝑥,𝑦,𝑧   𝐵,𝑔,ℎ,𝑧   𝑥,𝐹,𝑢,𝑣,𝑧   𝜑,𝑓,𝑧   𝑓,𝐹   𝜑,𝑔,ℎ,𝑥,𝑢,𝑣   𝐴,ℎ,𝑤,𝑓,𝑦,𝑥   𝑤,𝐺   𝑤,𝑅   𝑦,𝐹   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑦,𝑤)   𝐴(𝑣,𝑢,𝑔)   𝐵(𝑦,𝑤,𝑣,𝑢,𝑓)   𝐶(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑓,𝑔,ℎ)   𝑅(𝑣,𝑢,𝑔,ℎ)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑓,𝑔,ℎ)   𝐹(𝑤,𝑔,ℎ)   𝐺(𝑣,𝑢,𝑔,ℎ)

Proof of Theorem frrlem12

Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elun 4176	. . . 4 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
2		velsn 4664	. . . . 5 ⊢ (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
3	2	orbi2i 911	. . . 4 ⊢ ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
4	1, 3	bitri 275	. . 3 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
5		elinel2 4225	. . . . . . . 8 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ dom 𝐹)
6		frrlem11.1	. . . . . . . . . 10 ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
7	6	frrlem1 8327	. . . . . . . . 9 ⊢ 𝐵 = {𝑝 ∣ ∃𝑞(𝑝 Fn 𝑞 ∧ (𝑞 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑞 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑞) ∧ ∀𝑤 ∈ 𝑞 (𝑝‘𝑤) = (𝑤𝐺(𝑝 ↾ Pred(𝑅, 𝐴, 𝑤))))}
8		frrlem11.2	. . . . . . . . 9 ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)
9		breq1 5169	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → (𝑥𝑔𝑢 ↔ 𝑞𝑔𝑢))
10		breq1 5169	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → (𝑥ℎ𝑣 ↔ 𝑞ℎ𝑣))
11	9, 10	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑞 → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) ↔ (𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣)))
12	11	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑞 → (((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣) ↔ ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣)))
13	12	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑥 = 𝑞 → (((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) ↔ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣))))
14		frrlem11.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
15	13, 14	chvarvv 1998	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣))
16	7, 8, 15	frrlem10 8336	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝐹) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
17	5, 16	sylan2 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
18	17	adantlr 714	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
19		frrlem11.4	. . . . . . . . 9 ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
20	19	fveq1i 6921	. . . . . . . 8 ⊢ (𝐶‘𝑤) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤)
21	6, 8, 14	frrlem9 8335	. . . . . . . . . . . . 13 ⊢ (𝜑 → Fun 𝐹)
22	21	funresd 6621	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun (𝐹 ↾ 𝑆))
23		dmres 6041	. . . . . . . . . . . 12 ⊢ dom (𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹)
24		df-fn 6576	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝑆) ∧ dom (𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹)))
25	22, 23, 24	sylanblrc 589	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
26	25	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
27	26	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
28		vex 3492	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
29		ovex 7481	. . . . . . . . . . 11 ⊢ (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V
30	28, 29	fnsn 6636	. . . . . . . . . 10 ⊢ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧}
31	30	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
32		eldifn 4155	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹)
33		elinel2 4225	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑆 ∩ dom 𝐹) → 𝑧 ∈ dom 𝐹)
34	32, 33	nsyl 140	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
35		disjsn 4736	. . . . . . . . . . . 12 ⊢ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
36	34, 35	sylibr 234	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
37	36	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
38	37	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
39		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ (𝑆 ∩ dom 𝐹))
40		fvun1 7013	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹))) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
41	27, 31, 38, 39, 40	syl112anc 1374	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
42	20, 41	eqtrid 2792	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
43		elinel1 4224	. . . . . . . . 9 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ 𝑆)
44	43	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ 𝑆)
45	44	fvresd 6940	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹 ↾ 𝑆)‘𝑤) = (𝐹‘𝑤))
46	42, 45	eqtrd 2780	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = (𝐹‘𝑤))
47	6, 8, 14, 19	frrlem11 8337	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
48		fnfun 6679	. . . . . . . . . . 11 ⊢ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Fun 𝐶)
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Fun 𝐶)
50	49	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Fun 𝐶)
51		ssun1 4201	. . . . . . . . . . 11 ⊢ (𝐹 ↾ 𝑆) ⊆ ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
52	51, 19	sseqtrri 4046	. . . . . . . . . 10 ⊢ (𝐹 ↾ 𝑆) ⊆ 𝐶
53	52	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹 ↾ 𝑆) ⊆ 𝐶)
54		eldifi 4154	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴)
55		frrlem12.7	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
56	54, 55	sylan2 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
57		rspa 3254	. . . . . . . . . . . 12 ⊢ ((∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ 𝑤 ∈ 𝑆) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
58	56, 43, 57	syl2an 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
59	6, 8	frrlem8 8334	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
60	5, 59	syl 17	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
61	60	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
62	58, 61	ssind 4262	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
63	62, 23	sseqtrrdi 4060	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹 ↾ 𝑆))
64		fun2ssres 6623	. . . . . . . . 9 ⊢ ((Fun 𝐶 ∧ (𝐹 ↾ 𝑆) ⊆ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹 ↾ 𝑆)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
65	50, 53, 63, 64	syl3anc 1371	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
66	58	resabs1d 6037	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
67	65, 66	eqtrd 2780	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
68	67	oveq2d 7464	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
69	18, 46, 68	3eqtr4d 2790	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
70	69	ex 412	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ (𝑆 ∩ dom 𝐹) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
71	28, 29	fvsn 7215	. . . . . 6 ⊢ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
72	19	fveq1i 6921	. . . . . . 7 ⊢ (𝐶‘𝑧) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧)
73	30	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
74		vsnid 4685	. . . . . . . . 9 ⊢ 𝑧 ∈ {𝑧}
75	74	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ {𝑧})
76		fvun2 7014	. . . . . . . 8 ⊢ (((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
77	26, 73, 37, 75, 76	syl112anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
78	72, 77	eqtrid 2792	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
79	19	reseq1i 6005	. . . . . . . . 9 ⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧))
80		resundir 6024	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
81	79, 80	eqtri 2768	. . . . . . . 8 ⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
82		frrlem12.6	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
83	54, 82	sylan2 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
84	83	resabs1d 6037	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
85		frrlem12.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 Fr 𝐴)
86		predfrirr 6366	. . . . . . . . . . . . 13 ⊢ (𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
87	85, 86	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
88	87	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
89		ressnop0 7187	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
90	88, 89	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
91	84, 90	uneq12d 4192	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅))
92		un0 4417	. . . . . . . . 9 ⊢ ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))
93	91, 92	eqtrdi 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
94	81, 93	eqtrid 2792	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
95	94	oveq2d 7464	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))))
96	71, 78, 95	3eqtr4a 2806	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶‘𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
97		fveq2 6920	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝐶‘𝑤) = (𝐶‘𝑧))
98		id 22	. . . . . . 7 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
99		predeq3 6336	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
100	99	reseq2d 6009	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))
101	98, 100	oveq12d 7466	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
102	97, 101	eqeq12d 2756	. . . . 5 ⊢ (𝑤 = 𝑧 → ((𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶‘𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))))
103	96, 102	syl5ibrcom 247	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 = 𝑧 → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
104	70, 103	jaod 858	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
105	4, 104	biimtrid 242	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
106	105	3impia 1117	1 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 846   ∧ w3a 1087   = wceq 1537  ∃wex 1777   ∈ wcel 2108  {cab 2717  ∀wral 3067   ∖ cdif 3973   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  {csn 4648  ⟨cop 4654   class class class wbr 5166   Fr wfr 5649  dom cdm 5700   ↾ cres 5702  Predcpred 6331  Fun wfun 6567   Fn wfn 6568  ‘cfv 6573  (class class class)co 7448  frecscfrecs 8321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-id 5593  df-fr 5652  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-iota 6525  df-fun 6575  df-fn 6576  df-fv 6581  df-ov 7451  df-frecs 8322

This theorem is referenced by:  frrlem13  8339