Theorem frrlem12 8290

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 4107	. . . 4 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
2		velsn 4605	. . . . 5 ⊢ (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
3	2	orbi2i 925	. . . 4 ⊢ ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
4	1, 3	bitri 278	. . 3 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
5		elinel2 4155	. . . . . . . 8 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ dom 𝐹)
6		frrlem11.1	. . . . . . . . . 10 ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
7	6	frrlem1 8279	. . . . . . . . 9 ⊢ 𝐵 = {𝑝 ∣ ∃𝑞(𝑝 Fn 𝑞 ∧ (𝑞 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑞 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑞) ∧ ∀𝑤 ∈ 𝑞 (𝑝‘𝑤) = (𝑤𝐺(𝑝 ↾ Pred(𝑅, 𝐴, 𝑤))))}
8		frrlem11.2	. . . . . . . . 9 ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)
9		breq1 5112	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → (𝑥𝑔𝑢 ↔ 𝑞𝑔𝑢))
10		breq1 5112	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → (𝑥ℎ𝑣 ↔ 𝑞ℎ𝑣))
11	9, 10	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑞 → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) ↔ (𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣)))
12	11	imbi1d 344	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑞 → (((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣) ↔ ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣)))
13	12	imbi2d 343	. . . . . . . . . 10 ⊢ (𝑥 = 𝑞 → (((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) ↔ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣))))
14		frrlem11.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
15	13, 14	chvarvv 2019	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣))
16	7, 8, 15	frrlem10 8288	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝐹) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
17	5, 16	sylan2 604	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
18	17	adantlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
19		frrlem11.4	. . . . . . . . 9 ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
20	19	fveq1i 6882	. . . . . . . 8 ⊢ (𝐶‘𝑤) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤)
21	6, 8, 14	frrlem9 8287	. . . . . . . . . . . . 13 ⊢ (𝜑 → Fun 𝐹)
22	21	funresd 6579	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun (𝐹 ↾ 𝑆))
23		dmres 6011	. . . . . . . . . . . 12 ⊢ dom (𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹)
24		df-fn 6539	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝑆) ∧ dom (𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹)))
25	22, 23, 24	sylanblrc 601	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
26	25	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
27	26	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
28		vex 3459	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
29		ovex 7443	. . . . . . . . . . 11 ⊢ (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V
30	28, 29	fnsn 6594	. . . . . . . . . 10 ⊢ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧}
31	30	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
32		eldifn 4086	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹)
33		elinel2 4155	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑆 ∩ dom 𝐹) → 𝑧 ∈ dom 𝐹)
34	32, 33	nsyl 141	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
35		disjsn 4677	. . . . . . . . . . . 12 ⊢ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
36	34, 35	sylibr 237	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
37	36	adantl 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
38	37	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
39		simpr 489	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ (𝑆 ∩ dom 𝐹))
40		fvun1 6972	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹))) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
41	27, 31, 38, 39, 40	syl112anc 1401	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
42	20, 41	eqtrid 2810	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
43		elinel1 4154	. . . . . . . . 9 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ 𝑆)
44	43	adantl 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ 𝑆)
45	44	fvresd 6901	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹 ↾ 𝑆)‘𝑤) = (𝐹‘𝑤))
46	42, 45	eqtrd 2798	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = (𝐹‘𝑤))
47	6, 8, 14, 19	frrlem11 8289	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
48		fnfun 6635	. . . . . . . . . . 11 ⊢ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Fun 𝐶)
49	47, 48	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Fun 𝐶)
50	49	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Fun 𝐶)
51		ssun1 4131	. . . . . . . . . . 11 ⊢ (𝐹 ↾ 𝑆) ⊆ ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
52	51, 19	sseqtrri 3986	. . . . . . . . . 10 ⊢ (𝐹 ↾ 𝑆) ⊆ 𝐶
53	52	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹 ↾ 𝑆) ⊆ 𝐶)
54		eldifi 4085	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴)
55		frrlem12.7	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
56	54, 55	sylan2 604	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
57		rspa 3254	. . . . . . . . . . . 12 ⊢ ((∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ 𝑤 ∈ 𝑆) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
58	56, 43, 57	syl2an 607	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
59	6, 8	frrlem8 8286	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
60	5, 59	syl 18	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
61	60	adantl 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
62	58, 61	ssind 4193	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
63	62, 23	sseqtrrdi 3978	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹 ↾ 𝑆))
64		fun2ssres 6581	. . . . . . . . 9 ⊢ ((Fun 𝐶 ∧ (𝐹 ↾ 𝑆) ⊆ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹 ↾ 𝑆)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
65	50, 53, 63, 64	syl3anc 1398	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
66	58	resabs1d 6007	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
67	65, 66	eqtrd 2798	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
68	67	oveq2d 7426	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
69	18, 46, 68	3eqtr4d 2808	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
70	69	ex 417	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ (𝑆 ∩ dom 𝐹) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
71	28, 29	fvsn 7179	. . . . . 6 ⊢ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
72	19	fveq1i 6882	. . . . . . 7 ⊢ (𝐶‘𝑧) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧)
73	30	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
74		vsnid 4629	. . . . . . . . 9 ⊢ 𝑧 ∈ {𝑧}
75	74	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ {𝑧})
76		fvun2 6973	. . . . . . . 8 ⊢ (((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
77	26, 73, 37, 75, 76	syl112anc 1401	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
78	72, 77	eqtrid 2810	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
79	19	reseq1i 5974	. . . . . . . . 9 ⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧))
80		resundir 5993	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
81	79, 80	eqtri 2786	. . . . . . . 8 ⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
82		frrlem12.6	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
83	54, 82	sylan2 604	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
84	83	resabs1d 6007	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
85		frrlem12.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 Fr 𝐴)
86		predfrirr 6335	. . . . . . . . . . . . 13 ⊢ (𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
87	85, 86	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
88	87	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
89		ressnop0 7150	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
90	88, 89	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
91	84, 90	uneq12d 4123	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅))
92		un0 4351	. . . . . . . . 9 ⊢ ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))
93	91, 92	eqtrdi 2814	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
94	81, 93	eqtrid 2810	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
95	94	oveq2d 7426	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))))
96	71, 78, 95	3eqtr4a 2824	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶‘𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
97		fveq2 6881	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝐶‘𝑤) = (𝐶‘𝑧))
98		id 23	. . . . . . 7 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
99		predeq3 6306	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
100	99	reseq2d 5978	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))
101	98, 100	oveq12d 7428	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
102	97, 101	eqeq12d 2779	. . . . 5 ⊢ (𝑤 = 𝑧 → ((𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶‘𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))))
103	96, 102	syl5ibrcom 250	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 = 𝑧 → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
104	70, 103	jaod 872	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
105	4, 104	biimtrid 245	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
106	105	3impia 1135	1 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 400   ∨ wo 860   ∧ w3a 1103   = wceq 1570  ∃wex 1809   ∈ wcel 2143  {cab 2741  ∀wral 3079   ∖ cdif 3902   ∪ cun 3903   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  {csn 4589  ⟨cop 4595   class class class wbr 5109   Fr wfr 5611  dom cdm 5661   ↾ cres 5663  Predcpred 6301  Fun wfun 6530   Fn wfn 6531  ‘cfv 6536  (class class class)co 7410  frecscfrecs 8273

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-id 5556  df-fr 5614  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-iota 6492  df-fun 6538  df-fn 6539  df-fv 6544  df-ov 7413  df-frecs 8274

This theorem is used by:  frrlem13  8291