Theorem frrlem13 8295

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 4078	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴)
2		frrlem13.8	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ∈ V)
3	1, 2	sylan2 605	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑆 ∈ V)
4	3	adantrr 730	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑆 ∈ V)
5		inex1g 5279	. . . . 5 ⊢ (𝑆 ∈ V → (𝑆 ∩ dom 𝐹) ∈ V)
6		snex 5397	. . . . 5 ⊢ {𝑧} ∈ V
7		unexg 7744	. . . . 5 ⊢ (((𝑆 ∩ dom 𝐹) ∈ V ∧ {𝑧} ∈ V) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V)
8	5, 6, 7	sylancl 598	. . . 4 ⊢ (𝑆 ∈ V → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V)
9	4, 8	syl 18	. . 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 8293	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
15	14	adantrr 730	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
16		inss1 4182	. . . . . 6 ⊢ (𝑆 ∩ dom 𝐹) ⊆ 𝑆
17		frrlem13.9	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ⊆ 𝐴)
18	1, 17	sylan2 605	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑆 ⊆ 𝐴)
19	18	adantrr 730	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑆 ⊆ 𝐴)
20	16, 19	sstrid 3942	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑆 ∩ dom 𝐹) ⊆ 𝐴)
21	1	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ 𝐴)
22	21	adantrr 730	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑧 ∈ 𝐴)
23	22	snssd 4747	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → {𝑧} ⊆ 𝐴)
24	20, 23	unssd 4138	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴)
25		elun 4100	. . . . . . . . 9 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
26		elin 3915	. . . . . . . . . 10 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ↔ (𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹))
27		velsn 4600	. . . . . . . . . 10 ⊢ (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
28	26, 27	orbi12i 928	. . . . . . . . 9 ⊢ ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧))
29	25, 28	bitri 278	. . . . . . . 8 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧))
30		frrlem12.7	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
31	1, 30	sylan2 605	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
32	31	adantrr 730	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
33		rsp 3250	. . . . . . . . . . . 12 ⊢ (∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 → (𝑤 ∈ 𝑆 → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆))
34	32, 33	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 ∈ 𝑆 → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆))
35	10, 11	frrlem8 8290	. . . . . . . . . . 11 ⊢ (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
36	34, 35	anim12d1 622	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)))
37		ssin 4184	. . . . . . . . . 10 ⊢ ((Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹) ↔ Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
38	36, 37	imbitrdi 254	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
39		frrlem12.6	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
40	1, 39	sylan2 605	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
41	40	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
42		preddif 6322	. . . . . . . . . . . . . . . 16 ⊢ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧))
43	42	eqeq1i 2765	. . . . . . . . . . . . . . 15 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ ↔ (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧)) = ∅)
44		ssdif0 4314	. . . . . . . . . . . . . . 15 ⊢ (Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, dom 𝐹, 𝑧) ↔ (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧)) = ∅)
45	43, 44	sylbb2 241	. . . . . . . . . . . . . 14 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, dom 𝐹, 𝑧))
46		predss 6302	. . . . . . . . . . . . . 14 ⊢ Pred(𝑅, dom 𝐹, 𝑧) ⊆ dom 𝐹
47	45, 46	sstrdi 3943	. . . . . . . . . . . . 13 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
48	47	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
49	48	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
50	41, 49	ssind 4186	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ (𝑆 ∩ dom 𝐹))
51		predeq3 6298	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
52	51	sseq1d 3962	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → (Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹) ↔ Pred(𝑅, 𝐴, 𝑧) ⊆ (𝑆 ∩ dom 𝐹)))
53	50, 52	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
54	38, 53	jaod 873	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
55	29, 54	biimtrid 245	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
56	55	imp 412	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
57		ssun1 4124	. . . . . 6 ⊢ (𝑆 ∩ dom 𝐹) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})
58	56, 57	sstrdi 3943	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
59	58	ralrimiva 3154	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
60	24, 59	jca 521	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
61		frrlem12.5	. . . . . . 7 ⊢ (𝜑 → 𝑅 Fr 𝐴)
62	10, 11, 12, 13, 61, 39, 30	frrlem12 8294	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
63	62	3expa 1136	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
64	63	ralrimiva 3154	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
65	64	adantrr 730	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
66		fneq2 6620	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶 Fn 𝑡 ↔ 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
67		sseq1 3956	. . . . . . 7 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴))
68		sseq2 3957	. . . . . . . 8 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡 ↔ Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
69	68	raleqbi1dv 3329	. . . . . . 7 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡 ↔ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
70	67, 69	anbi12d 644	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ↔ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))))
71		raleq 3316	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
72	66, 70, 71	3anbi123d 1464	. . . . 5 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → ((𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
73	72	spcegv 3551	. . . 4 ⊢ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V → ((𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
74	73	imp 412	. . 3 ⊢ ((((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V ∧ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
75	9, 15, 60, 65, 74	syl13anc 1399	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
76	10, 11, 12	frrlem9 8291	. . . . . 6 ⊢ (𝜑 → Fun 𝐹)
77		resfunexg 7210	. . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝑆 ∈ V) → (𝐹 ↾ 𝑆) ∈ V)
78	76, 4, 77	syl2an2r 698	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝐹 ↾ 𝑆) ∈ V)
79		snex 5397	. . . . 5 ⊢ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ∈ V
80		unexg 7744	. . . . 5 ⊢ (((𝐹 ↾ 𝑆) ∈ V ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ∈ V) → ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∈ V)
81	78, 79, 80	sylancl 598	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∈ V)
82	13, 81	eqeltrid 2864	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ V)
83		fneq1 6619	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑐 Fn 𝑡 ↔ 𝐶 Fn 𝑡))
84		fveq1 6873	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘𝑤) = (𝐶‘𝑤))
85		reseq1 5961	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))
86	85	oveq2d 7425	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
87	84, 86	eqeq12d 2776	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
88	87	ralbidv 3185	. . . . . 6 ⊢ (𝑐 = 𝐶 → (∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
89	83, 88	3anbi13d 1466	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ (𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
90	89	exbidv 1954	. . . 4 ⊢ (𝑐 = 𝐶 → (∃𝑡(𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
91	10	frrlem1 8283	. . . 4 ⊢ 𝐵 = {𝑐 ∣ ∃𝑡(𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))))}
92	90, 91	elab2g 3634	. . 3 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐵 ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
93	82, 92	syl 18	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝐶 ∈ 𝐵 ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
94	75, 93	mpbird 260	1 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2738  ∀wral 3076  Vcvv 3450   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  {csn 4584  ⟨cop 4590   class class class wbr 5103   Fr wfr 5598  dom cdm 5648   ↾ cres 5650  Predcpred 6293  Fun wfun 6522   Fn wfn 6523  ‘cfv 6528  (class class class)co 7409  frecscfrecs 8277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-fr 5601  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6294  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-ov 7412  df-frecs 8278

This theorem is used by:  frrlem14  8296