Theorem dfrecs2 35914

Description: A quantifier-free definition of recs. (Contributed by Scott Fenton, 17-Jul-2020.)

Assertion

Ref	Expression
dfrecs2	⊢ recs(𝐹) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))))

Proof of Theorem dfrecs2

Dummy variables 𝑓 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfrecs3 8384	. 2 ⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
2		elin 3942	. . . . . . . . 9 ⊢ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)))
3		vex 3463	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
4	3	elfuns 35879	. . . . . . . . . 10 ⊢ (𝑓 ∈ Funs ↔ Fun 𝑓)
5		vex 3463	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
6	5, 3	brcnv 5862	. . . . . . . . . . . . 13 ⊢ (𝑥◡Domain𝑓 ↔ 𝑓Domain𝑥)
7	3, 5	brdomain 35897	. . . . . . . . . . . . 13 ⊢ (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓)
8	6, 7	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑥◡Domain𝑓 ↔ 𝑥 = dom 𝑓)
9	8	rexbii 3083	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ On 𝑥◡Domain𝑓 ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
10	3	elima 6052	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥◡Domain𝑓)
11		risset 3217	. . . . . . . . . . 11 ⊢ (dom 𝑓 ∈ On ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
12	9, 10, 11	3bitr4i 303	. . . . . . . . . 10 ⊢ (𝑓 ∈ (◡Domain “ On) ↔ dom 𝑓 ∈ On)
13	4, 12	anbi12i 628	. . . . . . . . 9 ⊢ ((𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
14	2, 13	bitri 275	. . . . . . . 8 ⊢ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
15	3	eldm 5880	. . . . . . . . . . 11 ⊢ (𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦 𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦)
16		brdif 5172	. . . . . . . . . . . . 13 ⊢ (𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑓(◡ E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦))
17		vex 3463	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
18	3, 17	brco 5850	. . . . . . . . . . . . . . 15 ⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦))
19	7	anbi1i 624	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
20	19	exbii 1848	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
21	3	dmex 7903	. . . . . . . . . . . . . . . . 17 ⊢ dom 𝑓 ∈ V
22		breq1 5122	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = dom 𝑓 → (𝑥◡ E 𝑦 ↔ dom 𝑓◡ E 𝑦))
23	21, 22	ceqsexv 3511	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
24	20, 23	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
25	21, 17	brcnv 5862	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑓◡ E 𝑦 ↔ 𝑦 E dom 𝑓)
26	21	epeli 5555	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓)
27	25, 26	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑓◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓)
28	18, 24, 27	3bitri 297	. . . . . . . . . . . . . 14 ⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ 𝑦 ∈ dom 𝑓)
29		df-br 5120	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ⟨𝑓, 𝑦⟩ ∈ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))
30		opex 5439	. . . . . . . . . . . . . . . . 17 ⊢ ⟨𝑓, 𝑦⟩ ∈ V
31	30	elfix 35867	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑓, 𝑦⟩ ∈ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)) ↔ ⟨𝑓, 𝑦⟩(◡Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩)
32	30, 30	brco 5850	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑓, 𝑦⟩(◡Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ ∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩))
33		ancom 460	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩) ↔ (𝑥◡Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
34	5, 30	brcnv 5862	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
35	3, 17, 5	brapply 35902	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑓, 𝑦⟩Apply𝑥 ↔ 𝑥 = (𝑓‘𝑦))
36	34, 35	bitri 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓‘𝑦))
37	36	anbi1i 624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥◡Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ (𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
38	33, 37	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
39	38	exbii 1848	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
40		fvex 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓‘𝑦) ∈ V
41		breq2 5123	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑦) → (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦)))
42	40, 41	ceqsexv 3511	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦))
43	39, 42	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦))
44	30, 40	brco 5850	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦) ↔ ∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
45	3, 17, 5	brrestrict 35913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑓, 𝑦⟩Restrict𝑥 ↔ 𝑥 = (𝑓 ↾ 𝑦))
46	45	anbi1i 624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
47	46	exbii 1848	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ ∃𝑥(𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
48	3	resex 6016	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ↾ 𝑦) ∈ V
49		breq1 5122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓 ↾ 𝑦) → (𝑥FullFun𝐹(𝑓‘𝑦) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦)))
50	48, 49	ceqsexv 3511	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦))
51	47, 50	bitri 275	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦))
52	48, 40	brfullfun 35912	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
53	44, 51, 52	3bitri 297	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
54	32, 43, 53	3bitri 297	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑓, 𝑦⟩(◡Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
55	29, 31, 54	3bitri 297	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
56	55	notbii 320	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑓 Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
57	28, 56	anbi12i 628	. . . . . . . . . . . . 13 ⊢ ((𝑓(◡ E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦) ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
58	16, 57	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
59	58	exbii 1848	. . . . . . . . . . 11 ⊢ (∃𝑦 𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
60	15, 59	bitri 275	. . . . . . . . . 10 ⊢ (𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
61		df-rex 3061	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ dom 𝑓 ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
62		rexnal 3089	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ dom 𝑓 ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ¬ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
63	60, 61, 62	3bitr2ri 300	. . . . . . . . 9 ⊢ (¬ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))))
64	63	con1bii 356	. . . . . . . 8 ⊢ (¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
65	14, 64	anbi12i 628	. . . . . . 7 ⊢ ((𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
66		anass 468	. . . . . . 7 ⊢ (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
67	65, 66	bitri 275	. . . . . 6 ⊢ ((𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
68		eleq1 2822	. . . . . . . . 9 ⊢ (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
69		raleq 3302	. . . . . . . . 9 ⊢ (𝑥 = dom 𝑓 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
70	68, 69	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
71	70	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))))
72	21, 71	ceqsexv 3511	. . . . . 6 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
73		df-fn 6533	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
74		eqcom 2742	. . . . . . . . . . 11 ⊢ (dom 𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓)
75	74	anbi2i 623	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (Fun 𝑓 ∧ 𝑥 = dom 𝑓))
76		ancom 460	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ 𝑥 = dom 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
77	73, 75, 76	3bitri 297	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
78	77	anbi1i 624	. . . . . . . 8 ⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
79		an12 645	. . . . . . . 8 ⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
80		anass 468	. . . . . . . 8 ⊢ (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))))
81	78, 79, 80	3bitr3ri 302	. . . . . . 7 ⊢ ((𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
82	81	exbii 1848	. . . . . 6 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
83	67, 72, 82	3bitr2i 299	. . . . 5 ⊢ ((𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
84		eldif 3936	. . . . 5 ⊢ (𝑓 ∈ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))))
85		df-rex 3061	. . . . 5 ⊢ (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
86	83, 84, 85	3bitr4i 303	. . . 4 ⊢ (𝑓 ∈ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
87	86	eqabi 2870	. . 3 ⊢ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
88	87	unieqi 4895	. 2 ⊢ ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
89	1, 88	eqtr4i 2761	1 ⊢ recs(𝐹) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))))

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  {cab 2713  ∀wral 3051  ∃wrex 3060   ∖ cdif 3923   ∩ cin 3925  ⟨cop 4607  ∪ cuni 4883   class class class wbr 5119   E cep 5552  ^◡ccnv 5653  dom cdm 5654   ↾ cres 5656   “ cima 5657   ∘ ccom 5658  Oncon0 6352  Fun wfun 6524   Fn wfn 6525  ‘cfv 6530  recscrecs 8382   Fix cfix 35799   Funs cfuns 35801  Domaincdomain 35807  Applycapply 35809  FullFuncfullfn 35814  Restrictcrestrict 35815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-symdif 4228  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fo 6536  df-fv 6538  df-ov 7406  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-txp 35818  df-pprod 35819  df-bigcup 35822  df-fix 35823  df-funs 35825  df-singleton 35826  df-singles 35827  df-image 35828  df-cart 35829  df-img 35830  df-domain 35831  df-range 35832  df-cap 35834  df-restrict 35835  df-apply 35837  df-funpart 35838  df-fullfun 35839

This theorem is referenced by: (None)