Theorem frrlem13 8339

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 4154	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴)
2		frrlem13.8	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ∈ V)
3	1, 2	sylan2 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑆 ∈ V)
4	3	adantrr 716	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑆 ∈ V)
5		inex1g 5337	. . . . 5 ⊢ (𝑆 ∈ V → (𝑆 ∩ dom 𝐹) ∈ V)
6		snex 5451	. . . . 5 ⊢ {𝑧} ∈ V
7		unexg 7778	. . . . 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 8337	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
15	14	adantrr 716	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
16		inss1 4258	. . . . . 6 ⊢ (𝑆 ∩ dom 𝐹) ⊆ 𝑆
17		frrlem13.9	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ⊆ 𝐴)
18	1, 17	sylan2 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑆 ⊆ 𝐴)
19	18	adantrr 716	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑆 ⊆ 𝐴)
20	16, 19	sstrid 4020	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑆 ∩ dom 𝐹) ⊆ 𝐴)
21	1	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧 ∈ 𝐴)
22	21	adantrr 716	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑧 ∈ 𝐴)
23	22	snssd 4834	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → {𝑧} ⊆ 𝐴)
24	20, 23	unssd 4215	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴)
25		elun 4176	. . . . . . . . 9 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
26		elin 3992	. . . . . . . . . 10 ⊢ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ↔ (𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹))
27		velsn 4664	. . . . . . . . . 10 ⊢ (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
28	26, 27	orbi12i 913	. . . . . . . . 9 ⊢ ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧))
29	25, 28	bitri 275	. . . . . . . 8 ⊢ (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧))
30		frrlem12.7	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
31	1, 30	sylan2 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
32	31	adantrr 716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
33		rsp 3253	. . . . . . . . . . . 12 ⊢ (∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 → (𝑤 ∈ 𝑆 → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆))
34	32, 33	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 ∈ 𝑆 → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆))
35	10, 11	frrlem8 8334	. . . . . . . . . . 11 ⊢ (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
36	34, 35	anim12d1 609	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)))
37		ssin 4260	. . . . . . . . . 10 ⊢ ((Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹) ↔ Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
38	36, 37	imbitrdi 251	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
39		frrlem12.6	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
40	1, 39	sylan2 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
41	40	adantrr 716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
42		preddif 6361	. . . . . . . . . . . . . . . 16 ⊢ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧))
43	42	eqeq1i 2745	. . . . . . . . . . . . . . 15 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ ↔ (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧)) = ∅)
44		ssdif0 4389	. . . . . . . . . . . . . . 15 ⊢ (Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, dom 𝐹, 𝑧) ↔ (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧)) = ∅)
45	43, 44	sylbb2 238	. . . . . . . . . . . . . 14 ⊢ (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, dom 𝐹, 𝑧))
46		predss 6340	. . . . . . . . . . . . . 14 ⊢ Pred(𝑅, dom 𝐹, 𝑧) ⊆ dom 𝐹
47	45, 46	sstrdi 4021	. . . . . . . . . . . . 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 4262	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ (𝑆 ∩ dom 𝐹))
51		predeq3 6336	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
52	51	sseq1d 4040	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → (Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹) ↔ Pred(𝑅, 𝐴, 𝑧) ⊆ (𝑆 ∩ dom 𝐹)))
53	50, 52	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
54	38, 53	jaod 858	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (((𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
55	29, 54	biimtrid 242	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
56	55	imp 406	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
57		ssun1 4201	. . . . . 6 ⊢ (𝑆 ∩ dom 𝐹) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})
58	56, 57	sstrdi 4021	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
59	58	ralrimiva 3152	. . . 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 8338	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
63	62	3expa 1118	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
64	63	ralrimiva 3152	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
65	64	adantrr 716	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
66		fneq2 6671	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶 Fn 𝑡 ↔ 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
67		sseq1 4034	. . . . . . 7 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝑡 ⊆ 𝐴 ↔ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴))
68		sseq2 4035	. . . . . . . 8 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡 ↔ Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
69	68	raleqbi1dv 3346	. . . . . . 7 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡 ↔ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
70	67, 69	anbi12d 631	. . . . . 6 ⊢ (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → ((𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ↔ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))))
71		raleq 3331	. . . . . 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 3610	. . . 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 1372	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
76	10, 11, 12	frrlem9 8335	. . . . . 6 ⊢ (𝜑 → Fun 𝐹)
77		resfunexg 7252	. . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝑆 ∈ V) → (𝐹 ↾ 𝑆) ∈ V)
78	76, 4, 77	syl2an2r 684	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝐹 ↾ 𝑆) ∈ V)
79		snex 5451	. . . . 5 ⊢ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ∈ V
80		unexg 7778	. . . . 5 ⊢ (((𝐹 ↾ 𝑆) ∈ V ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ∈ V) → ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∈ V)
81	78, 79, 80	sylancl 585	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∈ V)
82	13, 81	eqeltrid 2848	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ V)
83		fneq1 6670	. . . . . 6 ⊢ (𝑐 = 𝐶 → (𝑐 Fn 𝑡 ↔ 𝐶 Fn 𝑡))
84		fveq1 6919	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘𝑤) = (𝐶‘𝑤))
85		reseq1 6003	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))
86	85	oveq2d 7464	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
87	84, 86	eqeq12d 2756	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
88	87	ralbidv 3184	. . . . . 6 ⊢ (𝑐 = 𝐶 → (∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
89	83, 88	3anbi13d 1438	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ (𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
90	89	exbidv 1920	. . . 4 ⊢ (𝑐 = 𝐶 → (∃𝑡(𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
91	10	frrlem1 8327	. . . 4 ⊢ 𝐵 = {𝑐 ∣ ∃𝑡(𝑐 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝑐‘𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))))}
92	90, 91	elab2g 3696	. . 3 ⊢ (𝐶 ∈ V → (𝐶 ∈ 𝐵 ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
93	82, 92	syl 17	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝐶 ∈ 𝐵 ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤 ∈ 𝑡 (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
94	75, 93	mpbird 257	1 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∧ w3a 1087   = wceq 1537  ∃wex 1777   ∈ wcel 2108  {cab 2717  ∀wral 3067  Vcvv 3488   ∖ cdif 3973   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  {csn 4648  ⟨cop 4654   class class class wbr 5166   Fr wfr 5649  dom cdm 5700   ↾ cres 5702  Predcpred 6331  Fun wfun 6567   Fn wfn 6568  ‘cfv 6573  (class class class)co 7448  frecscfrecs 8321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-fr 5652  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-frecs 8322

This theorem is referenced by:  frrlem14  8340