Theorem frrlem13 8229

Description: Lemma for well-founded recursion. Assuming that 𝑆 is a subset of 𝐴 and that 𝑧 is 𝑅-minimal, then 𝐶 is an acceptable function. (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(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
frrlem13.8	⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ∈ V)
frrlem13.9	⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ⊆ 𝐴)

Assertion

Ref	Expression
frrlem13	⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ 𝐵)

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

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

Proof of Theorem frrlem13

Dummy variables 𝑐 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldifi 4086	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴)
2		frrlem13.8	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ∈ V)
3	1, 2	sylan2 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑆 ∈ V)
4	3	adantrr 715	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑆 ∈ V)
5		inex1g 5276	. . . . 5 ⊢ (𝑆 ∈ V → (𝑆 ∩ dom 𝐹) ∈ V)
6		snex 5388	. . . . 5 ⊢ {𝑧} ∈ V
7		unexg 7683	. . . . 5 ⊢ (((𝑆 ∩ dom 𝐹) ∈ V ∧ {𝑧} ∈ V) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V)
8	5, 6, 7	sylancl 586	. . . 4 ⊢ (𝑆 ∈ V → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V)
9	4, 8	syl 17	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V)
10		frrlem11.1	. . . . 5 ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
11		frrlem11.2	. . . . 5 ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)
12		frrlem11.3	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
13		frrlem11.4	. . . . 5 ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
14	10, 11, 12, 13	frrlem11 8227	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
15	14	adantrr 715	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
16		inss1 4188	. . . . . 6 ⊢ (𝑆 ∩ dom 𝐹) ⊆ 𝑆
17		frrlem13.9	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ⊆ 𝐴)
18	1, 17	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑆 ⊆ 𝐴)
19	18	adantrr 715	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑆 ⊆ 𝐴)
20	16, 19	sstrid 3955	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑆 ∩ dom 𝐹) ⊆ 𝐴)
21	1	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ 𝐴)
22	21	adantrr 715	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑧 ∈ 𝐴)
23	22	snssd 4769	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → {𝑧} ⊆ 𝐴)
24	20, 23	unssd 4146	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴)
25		elun 4108	. . . . . . . . 9 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
26		elin 3926	. . . . . . . . . 10 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ↔ (𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹))
27		velsn 4602	. . . . . . . . . 10 ⊢ (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
28	26, 27	orbi12i 913	. . . . . . . . 9 ⊢ ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧))
29	25, 28	bitri 274	. . . . . . . 8 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧))
30		frrlem12.7	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
31	1, 30	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
32	31	adantrr 715	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
33		rsp 3230	. . . . . . . . . . . 12 ⊢ (∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 → (𝑤 ∈ 𝑆 → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆))
34	32, 33	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 ∈ 𝑆 → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆))
35	10, 11	frrlem8 8224	. . . . . . . . . . 11 ⊢ (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
36	34, 35	anim12d1 610	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)))
37		ssin 4190	. . . . . . . . . 10 ⊢ ((Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹) ↔ Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
38	36, 37	syl6ib 250	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
39		frrlem12.6	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
40	1, 39	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
41	40	adantrr 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
42		preddif 6283	. . . . . . . . . . . . . . . 16 ⊢ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧))
43	42	eqeq1i 2741	. . . . . . . . . . . . . . 15 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ ↔ (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧)) = ∅)
44		ssdif0 4323	. . . . . . . . . . . . . . 15 ⊢ (Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, dom 𝐹, 𝑧) ↔ (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧)) = ∅)
45	43, 44	sylbb2 237	. . . . . . . . . . . . . 14 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, dom 𝐹, 𝑧))
46		predss 6261	. . . . . . . . . . . . . 14 ⊢ Pred(𝑅, dom 𝐹, 𝑧) ⊆ dom 𝐹
47	45, 46	sstrdi 3956	. . . . . . . . . . . . 13 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
48	47	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
49	48	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
50	41, 49	ssind 4192	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ (𝑆 ∩ dom 𝐹))
51		predeq3 6257	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
52	51	sseq1d 3975	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → (Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹) ↔ Pred(𝑅, 𝐴, 𝑧) ⊆ (𝑆 ∩ dom 𝐹)))
53	50, 52	syl5ibrcom 246	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
54	38, 53	jaod 857	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
55	29, 54	biimtrid 241	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
56	55	imp 407	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
57		ssun1 4132	. . . . . 6 ⊢ (𝑆 ∩ dom 𝐹) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})
58	56, 57	sstrdi 3956	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
59	58	ralrimiva 3143	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
60	24, 59	jca 512	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
61		frrlem12.5	. . . . . . 7 ⊢ (𝜑 → 𝑅 Fr 𝐴)
62	10, 11, 12, 13, 61, 39, 30	frrlem12 8228	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
63	62	3expa 1118	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
64	63	ralrimiva 3143	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
65	64	adantrr 715	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
66		fneq2 6594	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶 Fn 𝑡 ↔ 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
67		sseq1 3969	. . . . . . 7 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴))
68		sseq2 3970	. . . . . . . 8 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡 ↔ Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
69	68	raleqbi1dv 3307	. . . . . . 7 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡 ↔ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
70	67, 69	anbi12d 631	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ↔ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))))
71		raleq 3309	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
72	66, 70, 71	3anbi123d 1436	. . . . 5 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → ((𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
73	72	spcegv 3556	. . . 4 ⊢ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V → ((𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
74	73	imp 407	. . 3 ⊢ ((((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V ∧ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
75	9, 15, 60, 65, 74	syl13anc 1372	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
76	10, 11, 12	frrlem9 8225	. . . . . 6 ⊢ (𝜑 → Fun 𝐹)
77		resfunexg 7165	. . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝑆 ∈ V) → (𝐹 ↾ 𝑆) ∈ V)
78	76, 4, 77	syl2an2r 683	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝐹 ↾ 𝑆) ∈ V)
79		snex 5388	. . . . 5 ⊢ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ∈ V
80		unexg 7683	. . . . 5 ⊢ (((𝐹 ↾ 𝑆) ∈ V ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ∈ V) → ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∈ V)
81	78, 79, 80	sylancl 586	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∈ V)
82	13, 81	eqeltrid 2842	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ V)
83		fneq1 6593	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑐 Fn 𝑡 ↔ 𝐶 Fn 𝑡))
84		fveq1 6841	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘𝑤) = (𝐶‘𝑤))
85		reseq1 5931	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))
86	85	oveq2d 7373	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
87	84, 86	eqeq12d 2752	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
88	87	ralbidv 3174	. . . . . 6 ⊢ (𝑐 = 𝐶 → (∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
89	83, 88	3anbi13d 1438	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ (𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
90	89	exbidv 1924	. . . 4 ⊢ (𝑐 = 𝐶 → (∃𝑡(𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
91	10	frrlem1 8217	. . . 4 ⊢ 𝐵 = {𝑐 ∣ ∃𝑡(𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))))}
92	90, 91	elab2g 3632	. . 3 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐵 ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
93	82, 92	syl 17	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝐶 ∈ 𝐵 ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
94	75, 93	mpbird 256	1 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2713  ∀wral 3064  Vcvv 3445   ∖ cdif 3907   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  {csn 4586  ⟨cop 4592   class class class wbr 5105   Fr wfr 5585  dom cdm 5633   ↾ cres 5635  Predcpred 6252  Fun wfun 6490   Fn wfn 6491  ‘cfv 6496  (class class class)co 7357  frecscfrecs 8211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-fr 5588  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-frecs 8212

This theorem is referenced by:  frrlem14  8230