Theorem frrlem12 8301

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 4133	. . . 4 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
2		velsn 4622	. . . . 5 ⊢ (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
3	2	orbi2i 912	. . . 4 ⊢ ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
4	1, 3	bitri 275	. . 3 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
5		elinel2 4182	. . . . . . . 8 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ dom 𝐹)
6		frrlem11.1	. . . . . . . . . 10 ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
7	6	frrlem1 8290	. . . . . . . . 9 ⊢ 𝐵 = {𝑝 ∣ ∃𝑞(𝑝 Fn 𝑞 ∧ (𝑞 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑞 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑞) ∧ ∀𝑤 ∈ 𝑞 (𝑝‘𝑤) = (𝑤𝐺(𝑝 ↾ Pred(𝑅, 𝐴, 𝑤))))}
8		frrlem11.2	. . . . . . . . 9 ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)
9		breq1 5127	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → (𝑥𝑔𝑢 ↔ 𝑞𝑔𝑢))
10		breq1 5127	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → (𝑥ℎ𝑣 ↔ 𝑞ℎ𝑣))
11	9, 10	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑞 → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) ↔ (𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣)))
12	11	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑞 → (((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣) ↔ ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣)))
13	12	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑥 = 𝑞 → (((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) ↔ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣))))
14		frrlem11.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
15	13, 14	chvarvv 1989	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣))
16	7, 8, 15	frrlem10 8299	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝐹) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
17	5, 16	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
18	17	adantlr 715	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
19		frrlem11.4	. . . . . . . . 9 ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
20	19	fveq1i 6882	. . . . . . . 8 ⊢ (𝐶‘𝑤) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤)
21	6, 8, 14	frrlem9 8298	. . . . . . . . . . . . 13 ⊢ (𝜑 → Fun 𝐹)
22	21	funresd 6584	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun (𝐹 ↾ 𝑆))
23		dmres 6004	. . . . . . . . . . . 12 ⊢ dom (𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹)
24		df-fn 6539	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝑆) ∧ dom (𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹)))
25	22, 23, 24	sylanblrc 590	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
26	25	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
27	26	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
28		vex 3468	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
29		ovex 7443	. . . . . . . . . . 11 ⊢ (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V
30	28, 29	fnsn 6599	. . . . . . . . . 10 ⊢ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧}
31	30	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
32		eldifn 4112	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹)
33		elinel2 4182	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑆 ∩ dom 𝐹) → 𝑧 ∈ dom 𝐹)
34	32, 33	nsyl 140	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
35		disjsn 4692	. . . . . . . . . . . 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 6975	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹))) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
41	27, 31, 38, 39, 40	syl112anc 1376	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
42	20, 41	eqtrid 2783	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
43		elinel1 4181	. . . . . . . . 9 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ 𝑆)
44	43	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ 𝑆)
45	44	fvresd 6901	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹 ↾ 𝑆)‘𝑤) = (𝐹‘𝑤))
46	42, 45	eqtrd 2771	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = (𝐹‘𝑤))
47	6, 8, 14, 19	frrlem11 8300	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
48		fnfun 6643	. . . . . . . . . . 11 ⊢ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Fun 𝐶)
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Fun 𝐶)
50	49	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Fun 𝐶)
51		ssun1 4158	. . . . . . . . . . 11 ⊢ (𝐹 ↾ 𝑆) ⊆ ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
52	51, 19	sseqtrri 4013	. . . . . . . . . 10 ⊢ (𝐹 ↾ 𝑆) ⊆ 𝐶
53	52	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹 ↾ 𝑆) ⊆ 𝐶)
54		eldifi 4111	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴)
55		frrlem12.7	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
56	54, 55	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
57		rspa 3235	. . . . . . . . . . . 12 ⊢ ((∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ 𝑤 ∈ 𝑆) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
58	56, 43, 57	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
59	6, 8	frrlem8 8297	. . . . . . . . . . . . 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 4221	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
63	62, 23	sseqtrrdi 4005	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹 ↾ 𝑆))
64		fun2ssres 6586	. . . . . . . . 9 ⊢ ((Fun 𝐶 ∧ (𝐹 ↾ 𝑆) ⊆ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹 ↾ 𝑆)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
65	50, 53, 63, 64	syl3anc 1373	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
66	58	resabs1d 6000	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
67	65, 66	eqtrd 2771	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
68	67	oveq2d 7426	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
69	18, 46, 68	3eqtr4d 2781	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
70	69	ex 412	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ (𝑆 ∩ dom 𝐹) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
71	28, 29	fvsn 7178	. . . . . 6 ⊢ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
72	19	fveq1i 6882	. . . . . . 7 ⊢ (𝐶‘𝑧) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧)
73	30	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
74		vsnid 4644	. . . . . . . . 9 ⊢ 𝑧 ∈ {𝑧}
75	74	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ {𝑧})
76		fvun2 6976	. . . . . . . 8 ⊢ (((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
77	26, 73, 37, 75, 76	syl112anc 1376	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
78	72, 77	eqtrid 2783	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
79	19	reseq1i 5967	. . . . . . . . 9 ⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧))
80		resundir 5986	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
81	79, 80	eqtri 2759	. . . . . . . 8 ⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
82		frrlem12.6	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
83	54, 82	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
84	83	resabs1d 6000	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
85		frrlem12.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 Fr 𝐴)
86		predfrirr 6328	. . . . . . . . . . . . 13 ⊢ (𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
87	85, 86	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
88	87	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
89		ressnop0 7148	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
90	88, 89	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
91	84, 90	uneq12d 4149	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅))
92		un0 4374	. . . . . . . . 9 ⊢ ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))
93	91, 92	eqtrdi 2787	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
94	81, 93	eqtrid 2783	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
95	94	oveq2d 7426	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))))
96	71, 78, 95	3eqtr4a 2797	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶‘𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
97		fveq2 6881	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝐶‘𝑤) = (𝐶‘𝑧))
98		id 22	. . . . . . 7 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
99		predeq3 6299	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
100	99	reseq2d 5971	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))
101	98, 100	oveq12d 7428	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
102	97, 101	eqeq12d 2752	. . . . 5 ⊢ (𝑤 = 𝑧 → ((𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶‘𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))))
103	96, 102	syl5ibrcom 247	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 = 𝑧 → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
104	70, 103	jaod 859	. . 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 847   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2714  ∀wral 3052   ∖ cdif 3928   ∪ cun 3929   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313  {csn 4606  ⟨cop 4612   class class class wbr 5124   Fr wfr 5608  dom cdm 5659   ↾ cres 5661  Predcpred 6294  Fun wfun 6530   Fn wfn 6531  ‘cfv 6536  (class class class)co 7410  frecscfrecs 8284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-id 5553  df-fr 5611  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-iota 6489  df-fun 6538  df-fn 6539  df-fv 6544  df-ov 7413  df-frecs 8285

This theorem is referenced by:  frrlem13  8302