Theorem dfrecs2 35931

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 8410	. 2 ⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
2		elin 3978	. . . . . . . . 9 ⊢ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)))
3		vex 3481	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
4	3	elfuns 35896	. . . . . . . . . 10 ⊢ (𝑓 ∈ Funs ↔ Fun 𝑓)
5		vex 3481	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
6	5, 3	brcnv 5895	. . . . . . . . . . . . 13 ⊢ (𝑥◡Domain𝑓 ↔ 𝑓Domain𝑥)
7	3, 5	brdomain 35914	. . . . . . . . . . . . 13 ⊢ (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓)
8	6, 7	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑥◡Domain𝑓 ↔ 𝑥 = dom 𝑓)
9	8	rexbii 3091	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ On 𝑥◡Domain𝑓 ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
10	3	elima 6084	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥◡Domain𝑓)
11		risset 3230	. . . . . . . . . . 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 5913	. . . . . . . . . . 11 ⊢ (𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦 𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦)
16		brdif 5200	. . . . . . . . . . . . 13 ⊢ (𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑓(◡ E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦))
17		vex 3481	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
18	3, 17	brco 5883	. . . . . . . . . . . . . . 15 ⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦))
19	7	anbi1i 624	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
20	19	exbii 1844	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
21	3	dmex 7931	. . . . . . . . . . . . . . . . 17 ⊢ dom 𝑓 ∈ V
22		breq1 5150	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = dom 𝑓 → (𝑥◡ E 𝑦 ↔ dom 𝑓◡ E 𝑦))
23	21, 22	ceqsexv 3529	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
24	20, 23	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
25	21, 17	brcnv 5895	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑓◡ E 𝑦 ↔ 𝑦 E dom 𝑓)
26	21	epeli 5590	. . . . . . . . . . . . . . . 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 5148	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ⟨𝑓, 𝑦⟩ ∈ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))
30		opex 5474	. . . . . . . . . . . . . . . . 17 ⊢ ⟨𝑓, 𝑦⟩ ∈ V
31	30	elfix 35884	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑓, 𝑦⟩ ∈ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)) ↔ ⟨𝑓, 𝑦⟩(◡Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩)
32	30, 30	brco 5883	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑓, 𝑦⟩(◡Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ ∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩))
33		ancom 460	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩) ↔ (𝑥◡Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
34	5, 30	brcnv 5895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
35	3, 17, 5	brapply 35919	. . . . . . . . . . . . . . . . . . . . . 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 1844	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
40		fvex 6919	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓‘𝑦) ∈ V
41		breq2 5151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑦) → (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦)))
42	40, 41	ceqsexv 3529	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦))
43	39, 42	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦))
44	30, 40	brco 5883	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦) ↔ ∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
45	3, 17, 5	brrestrict 35930	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑓, 𝑦⟩Restrict𝑥 ↔ 𝑥 = (𝑓 ↾ 𝑦))
46	45	anbi1i 624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
47	46	exbii 1844	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ ∃𝑥(𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
48	3	resex 6048	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ↾ 𝑦) ∈ V
49		breq1 5150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓 ↾ 𝑦) → (𝑥FullFun𝐹(𝑓‘𝑦) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦)))
50	48, 49	ceqsexv 3529	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦))
51	47, 50	bitri 275	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦))
52	48, 40	brfullfun 35929	. . . . . . . . . . . . . . . . . 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 1844	. . . . . . . . . . 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 3068	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ dom 𝑓 ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
62		rexnal 3097	. . . . . . . . . 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 2826	. . . . . . . . 9 ⊢ (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
69		raleq 3320	. . . . . . . . 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 3529	. . . . . 6 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
73		df-fn 6565	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
74		eqcom 2741	. . . . . . . . . . 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 1844	. . . . . 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 3972	. . . . 5 ⊢ (𝑓 ∈ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))))
85		df-rex 3068	. . . . 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 2874	. . 3 ⊢ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
88	87	unieqi 4923	. 2 ⊢ ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
89	1, 88	eqtr4i 2765	1 ⊢ recs(𝐹) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))))

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1536  ∃wex 1775   ∈ wcel 2105  {cab 2711  ∀wral 3058  ∃wrex 3067   ∖ cdif 3959   ∩ cin 3961  ⟨cop 4636  ∪ cuni 4911   class class class wbr 5147   E cep 5587  ^◡ccnv 5687  dom cdm 5688   ↾ cres 5690   “ cima 5691   ∘ ccom 5692  Oncon0 6385  Fun wfun 6556   Fn wfn 6557  ‘cfv 6562  recscrecs 8408   Fix cfix 35816   Funs cfuns 35818  Domaincdomain 35824  Applycapply 35826  FullFuncfullfn 35831  Restrictcrestrict 35832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-symdif 4258  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fo 6568  df-fv 6570  df-ov 7433  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-txp 35835  df-pprod 35836  df-bigcup 35839  df-fix 35840  df-funs 35842  df-singleton 35843  df-singles 35844  df-image 35845  df-cart 35846  df-img 35847  df-domain 35848  df-range 35849  df-cap 35851  df-restrict 35852  df-apply 35854  df-funpart 35855  df-fullfun 35856

This theorem is referenced by: (None)