Theorem frrlem12 32743

Description: Lemma for 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 4046	. . . 4 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
2		velsn 4488	. . . . 5 ⊢ (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
3	2	orbi2i 907	. . . 4 ⊢ ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
4	1, 3	bitri 276	. . 3 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧))
5		elinel2 4094	. . . . . . . 8 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ dom 𝐹)
6		frrlem11.1	. . . . . . . . . 10 ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
7	6	frrlem1 32732	. . . . . . . . 9 ⊢ 𝐵 = {𝑝 ∣ ∃𝑞(𝑝 Fn 𝑞 ∧ (𝑞 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑞 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑞) ∧ ∀𝑤 ∈ 𝑞 (𝑝‘𝑤) = (𝑤𝐺(𝑝 ↾ Pred(𝑅, 𝐴, 𝑤))))}
8		frrlem11.2	. . . . . . . . 9 ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)
9		breq1 4965	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → (𝑥𝑔𝑢 ↔ 𝑞𝑔𝑢))
10		breq1 4965	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑞 → (𝑥ℎ𝑣 ↔ 𝑞ℎ𝑣))
11	9, 10	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑞 → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) ↔ (𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣)))
12	11	imbi1d 343	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑞 → (((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣) ↔ ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣)))
13	12	imbi2d 342	. . . . . . . . . 10 ⊢ (𝑥 = 𝑞 → (((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) ↔ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣))))
14		frrlem11.3	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
15	13, 14	chvarv 2370	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑞𝑔𝑢 ∧ 𝑞ℎ𝑣) → 𝑢 = 𝑣))
16	7, 8, 15	frrlem10 32741	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝐹) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
17	5, 16	sylan2 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
18	17	adantlr 711	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹‘𝑤) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
19		frrlem11.4	. . . . . . . . 9 ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
20	19	fveq1i 6539	. . . . . . . 8 ⊢ (𝐶‘𝑤) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤)
21	6, 8, 14	frrlem9 32740	. . . . . . . . . . . . 13 ⊢ (𝜑 → Fun 𝐹)
22		funres 6267	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝑆))
23	21, 22	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun (𝐹 ↾ 𝑆))
24		dmres 5756	. . . . . . . . . . . 12 ⊢ dom (𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹)
25		df-fn 6228	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝑆) ∧ dom (𝐹 ↾ 𝑆) = (𝑆 ∩ dom 𝐹)))
26	23, 24, 25	sylanblrc 590	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
27	26	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
28	27	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹))
29		vex 3440	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
30		ovex 7048	. . . . . . . . . . 11 ⊢ (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V
31	29, 30	fnsn 6282	. . . . . . . . . 10 ⊢ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧}
32	31	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
33		eldifn 4025	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹)
34		elinel2 4094	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝑆 ∩ dom 𝐹) → 𝑧 ∈ dom 𝐹)
35	33, 34	nsyl 142	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
36		disjsn 4554	. . . . . . . . . . . 12 ⊢ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑆 ∩ dom 𝐹))
37	35, 36	sylibr 235	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
38	37	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
39	38	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅)
40		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ (𝑆 ∩ dom 𝐹))
41		fvun1 6621	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹))) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
42	28, 32, 39, 40, 41	syl112anc 1367	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
43	20, 42	syl5eq 2843	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = ((𝐹 ↾ 𝑆)‘𝑤))
44		elinel1 4093	. . . . . . . . 9 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → 𝑤 ∈ 𝑆)
45	44	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → 𝑤 ∈ 𝑆)
46	45	fvresd 6558	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹 ↾ 𝑆)‘𝑤) = (𝐹‘𝑤))
47	43, 46	eqtrd 2831	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = (𝐹‘𝑤))
48	6, 8, 14, 19	frrlem11 32742	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
49		fnfun 6323	. . . . . . . . . . 11 ⊢ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Fun 𝐶)
50	48, 49	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Fun 𝐶)
51	50	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Fun 𝐶)
52		ssun1 4069	. . . . . . . . . . 11 ⊢ (𝐹 ↾ 𝑆) ⊆ ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
53	52, 19	sseqtr4i 3925	. . . . . . . . . 10 ⊢ (𝐹 ↾ 𝑆) ⊆ 𝐶
54	53	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐹 ↾ 𝑆) ⊆ 𝐶)
55		eldifi 4024	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴)
56		frrlem12.7	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
57	55, 56	sylan2 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
58		rspa 3173	. . . . . . . . . . . 12 ⊢ ((∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ 𝑤 ∈ 𝑆) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
59	57, 44, 58	syl2an 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
60	6, 8	frrlem8 32739	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
61	5, 60	syl 17	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
62	61	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
63	59, 62	ssind 4129	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
64	63, 24	syl6sseqr 3939	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹 ↾ 𝑆))
65		fun2ssres 6269	. . . . . . . . 9 ⊢ ((Fun 𝐶 ∧ (𝐹 ↾ 𝑆) ⊆ 𝐶 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom (𝐹 ↾ 𝑆)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
66	51, 54, 64, 65	syl3anc 1364	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)))
67	59	resabs1d 5765	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
68	66, 67	eqtrd 2831	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑤)))
69	68	oveq2d 7032	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑤))))
70	18, 47, 69	3eqtr4d 2841	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ (𝑆 ∩ dom 𝐹)) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
71	70	ex 413	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ (𝑆 ∩ dom 𝐹) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
72	29, 30	fvsn 6806	. . . . . 6 ⊢ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
73	19	fveq1i 6539	. . . . . . 7 ⊢ (𝐶‘𝑧) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧)
74	31	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧})
75		vsnid 4507	. . . . . . . . 9 ⊢ 𝑧 ∈ {𝑧}
76	75	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ {𝑧})
77		fvun2 6622	. . . . . . . 8 ⊢ (((𝐹 ↾ 𝑆) Fn (𝑆 ∩ dom 𝐹) ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} Fn {𝑧} ∧ (((𝑆 ∩ dom 𝐹) ∩ {𝑧}) = ∅ ∧ 𝑧 ∈ {𝑧})) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
78	27, 74, 38, 76, 77	syl112anc 1367	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
79	73, 78	syl5eq 2843	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶‘𝑧) = ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}‘𝑧))
80	19	reseq1i 5730	. . . . . . . . 9 ⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧))
81		resundir 5749	. . . . . . . . 9 ⊢ (((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
82	80, 81	eqtri 2819	. . . . . . . 8 ⊢ (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)))
83		frrlem12.6	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
84	55, 83	sylan2 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
85	84	resabs1d 5765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
86		frrlem12.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 Fr 𝐴)
87		predfrirr 6052	. . . . . . . . . . . . 13 ⊢ (𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
88	86, 87	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
89	88	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧))
90		ressnop0 6778	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑧) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
91	89, 90	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧)) = ∅)
92	85, 91	uneq12d 4061	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅))
93		un0 4264	. . . . . . . . 9 ⊢ ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ∅) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))
94	92, 93	syl6eq 2847	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (((𝐹 ↾ 𝑆) ↾ Pred(𝑅, 𝐴, 𝑧)) ∪ ({⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
95	82, 94	syl5eq 2843	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
96	95	oveq2d 7032	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))))
97	72, 79, 96	3eqtr4a 2857	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝐶‘𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
98		fveq2 6538	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝐶‘𝑤) = (𝐶‘𝑧))
99		id 22	. . . . . . 7 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
100		predeq3 6027	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
101	100	reseq2d 5734	. . . . . . 7 ⊢ (𝑤 = 𝑧 → (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))
102	99, 101	oveq12d 7034	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧))))
103	98, 102	eqeq12d 2810	. . . . 5 ⊢ (𝑤 = 𝑧 → ((𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶‘𝑧) = (𝑧𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑧)))))
104	97, 103	syl5ibrcom 248	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 = 𝑧 → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
105	71, 104	jaod 854	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 = 𝑧) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
106	4, 105	syl5bi 243	. 2 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
107	106	3impia 1110	1 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 842   ∧ w3a 1080   = wceq 1522  ∃wex 1761   ∈ wcel 2081  {cab 2775  ∀wral 3105   ∖ cdif 3856   ∪ cun 3857   ∩ cin 3858   ⊆ wss 3859  ∅c0 4211  {csn 4472  ⟨cop 4478   class class class wbr 4962   Fr wfr 5399  dom cdm 5443   ↾ cres 5445  Predcpred 6022  Fun wfun 6219   Fn wfn 6220  ‘cfv 6225  (class class class)co 7016  frecscfrecs 32726

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-id 5348  df-fr 5402  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-iota 6189  df-fun 6227  df-fn 6228  df-fv 6233  df-ov 7019  df-frecs 32727

This theorem is referenced by:  frrlem13  32744