Theorem frrlem13 8085

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 4057	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴)
2		frrlem13.8	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ∈ V)
3	1, 2	sylan2 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑆 ∈ V)
4	3	adantrr 713	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑆 ∈ V)
5		inex1g 5238	. . . . 5 ⊢ (𝑆 ∈ V → (𝑆 ∩ dom 𝐹) ∈ V)
6		snex 5349	. . . . 5 ⊢ {𝑧} ∈ V
7		unexg 7577	. . . . 5 ⊢ (((𝑆 ∩ dom 𝐹) ∈ V ∧ {𝑧} ∈ V) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V)
8	5, 6, 7	sylancl 585	. . . 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 8083	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
15	14	adantrr 713	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
16		inss1 4159	. . . . . 6 ⊢ (𝑆 ∩ dom 𝐹) ⊆ 𝑆
17		frrlem13.9	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ⊆ 𝐴)
18	1, 17	sylan2 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑆 ⊆ 𝐴)
19	18	adantrr 713	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑆 ⊆ 𝐴)
20	16, 19	sstrid 3928	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑆 ∩ dom 𝐹) ⊆ 𝐴)
21	1	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ 𝐴)
22	21	adantrr 713	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑧 ∈ 𝐴)
23	22	snssd 4739	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → {𝑧} ⊆ 𝐴)
24	20, 23	unssd 4116	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴)
25		elun 4079	. . . . . . . . 9 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
26		elin 3899	. . . . . . . . . 10 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ↔ (𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹))
27		velsn 4574	. . . . . . . . . 10 ⊢ (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
28	26, 27	orbi12i 911	. . . . . . . . 9 ⊢ ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧))
29	25, 28	bitri 274	. . . . . . . 8 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧))
30		frrlem12.7	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
31	1, 30	sylan2 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
32	31	adantrr 713	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
33		rsp 3129	. . . . . . . . . . . 12 ⊢ (∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 → (𝑤 ∈ 𝑆 → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆))
34	32, 33	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 ∈ 𝑆 → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆))
35	10, 11	frrlem8 8080	. . . . . . . . . . 11 ⊢ (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
36	34, 35	anim12d1 609	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)))
37		ssin 4161	. . . . . . . . . 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 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
41	40	adantrr 713	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
42		preddif 6221	. . . . . . . . . . . . . . . 16 ⊢ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧))
43	42	eqeq1i 2743	. . . . . . . . . . . . . . 15 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ ↔ (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧)) = ∅)
44		ssdif0 4294	. . . . . . . . . . . . . . 15 ⊢ (Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, dom 𝐹, 𝑧) ↔ (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧)) = ∅)
45	43, 44	sylbb2 237	. . . . . . . . . . . . . 14 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, dom 𝐹, 𝑧))
46		predss 6199	. . . . . . . . . . . . . 14 ⊢ Pred(𝑅, dom 𝐹, 𝑧) ⊆ dom 𝐹
47	45, 46	sstrdi 3929	. . . . . . . . . . . . 13 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
48	47	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
49	48	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
50	41, 49	ssind 4163	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ (𝑆 ∩ dom 𝐹))
51		predeq3 6195	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
52	51	sseq1d 3948	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → (Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹) ↔ Pred(𝑅, 𝐴, 𝑧) ⊆ (𝑆 ∩ dom 𝐹)))
53	50, 52	syl5ibrcom 246	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
54	38, 53	jaod 855	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
55	29, 54	syl5bi 241	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
56	55	imp 406	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
57		ssun1 4102	. . . . . 6 ⊢ (𝑆 ∩ dom 𝐹) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})
58	56, 57	sstrdi 3929	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
59	58	ralrimiva 3107	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
60	24, 59	jca 511	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
61		frrlem12.5	. . . . . . 7 ⊢ (𝜑 → 𝑅 Fr 𝐴)
62	10, 11, 12, 13, 61, 39, 30	frrlem12 8084	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
63	62	3expa 1116	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
64	63	ralrimiva 3107	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
65	64	adantrr 713	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
66		fneq2 6509	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶 Fn 𝑡 ↔ 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
67		sseq1 3942	. . . . . . 7 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴))
68		sseq2 3943	. . . . . . . 8 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡 ↔ Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
69	68	raleqbi1dv 3331	. . . . . . 7 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡 ↔ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
70	67, 69	anbi12d 630	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ↔ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))))
71		raleq 3333	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
72	66, 70, 71	3anbi123d 1434	. . . . 5 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → ((𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
73	72	spcegv 3526	. . . 4 ⊢ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V → ((𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
74	73	imp 406	. . 3 ⊢ ((((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V ∧ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
75	9, 15, 60, 65, 74	syl13anc 1370	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
76	10, 11, 12	frrlem9 8081	. . . . . 6 ⊢ (𝜑 → Fun 𝐹)
77		resfunexg 7073	. . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝑆 ∈ V) → (𝐹 ↾ 𝑆) ∈ V)
78	76, 4, 77	syl2an2r 681	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝐹 ↾ 𝑆) ∈ V)
79		snex 5349	. . . . 5 ⊢ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ∈ V
80		unexg 7577	. . . . 5 ⊢ (((𝐹 ↾ 𝑆) ∈ V ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ∈ V) → ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∈ V)
81	78, 79, 80	sylancl 585	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∈ V)
82	13, 81	eqeltrid 2843	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ V)
83		fneq1 6508	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑐 Fn 𝑡 ↔ 𝐶 Fn 𝑡))
84		fveq1 6755	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘𝑤) = (𝐶‘𝑤))
85		reseq1 5874	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))
86	85	oveq2d 7271	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
87	84, 86	eqeq12d 2754	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
88	87	ralbidv 3120	. . . . . 6 ⊢ (𝑐 = 𝐶 → (∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
89	83, 88	3anbi13d 1436	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ (𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
90	89	exbidv 1925	. . . 4 ⊢ (𝑐 = 𝐶 → (∃𝑡(𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
91	10	frrlem1 8073	. . . 4 ⊢ 𝐵 = {𝑐 ∣ ∃𝑡(𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))))}
92	90, 91	elab2g 3604	. . 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 395   ∨ wo 843   ∧ w3a 1085   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715  ∀wral 3063  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  {csn 4558  ⟨cop 4564   class class class wbr 5070   Fr wfr 5532  dom cdm 5580   ↾ cres 5582  Predcpred 6190  Fun wfun 6412   Fn wfn 6413  ‘cfv 6418  (class class class)co 7255  frecscfrecs 8067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-fr 5535  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-frecs 8068

This theorem is referenced by:  frrlem14  8086