dfrecs2 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dfrecs2		Structured version Visualization version GIF version

Theorem dfrecs2 34922

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 8372	. 2 ⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
2		elin 3965	. . . . . . . . 9 ⊢ (𝑓 ∈ ( Funs ∩ (^◡Domain “ On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (^◡Domain “ On)))
3		vex 3479	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
4	3	elfuns 34887	. . . . . . . . . 10 ⊢ (𝑓 ∈ Funs ↔ Fun 𝑓)
5		vex 3479	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
6	5, 3	brcnv 5883	. . . . . . . . . . . . 13 ⊢ (𝑥^◡Domain𝑓 ↔ 𝑓Domain𝑥)
7	3, 5	brdomain 34905	. . . . . . . . . . . . 13 ⊢ (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓)
8	6, 7	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑥^◡Domain𝑓 ↔ 𝑥 = dom 𝑓)
9	8	rexbii 3095	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ On 𝑥^◡Domain𝑓 ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
10	3	elima 6065	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (^◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥^◡Domain𝑓)
11		risset 3231	. . . . . . . . . . 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 5901	. . . . . . . . . . 11 ⊢ (𝑓 ∈ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦 𝑓((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦)
16		brdif 5202	. . . . . . . . . . . . 13 ⊢ (𝑓((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑓(^◡ E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦))
17		vex 3479	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
18	3, 17	brco 5871	. . . . . . . . . . . . . . 15 ⊢ (𝑓(^◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥^◡ E 𝑦))
19	7	anbi1i 625	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓Domain𝑥 ∧ 𝑥^◡ E 𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥^◡ E 𝑦))
20	19	exbii 1851	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥^◡ E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥^◡ E 𝑦))
21	3	dmex 7902	. . . . . . . . . . . . . . . . 17 ⊢ dom 𝑓 ∈ V
22		breq1 5152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = dom 𝑓 → (𝑥^◡ E 𝑦 ↔ dom 𝑓^◡ E 𝑦))
23	21, 22	ceqsexv 3526	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥^◡ E 𝑦) ↔ dom 𝑓^◡ E 𝑦)
24	20, 23	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥^◡ E 𝑦) ↔ dom 𝑓^◡ E 𝑦)
25	21, 17	brcnv 5883	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑓^◡ E 𝑦 ↔ 𝑦 E dom 𝑓)
26	21	epeli 5583	. . . . . . . . . . . . . . . 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 5150	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ⟨𝑓, 𝑦⟩ ∈ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))
30		opex 5465	. . . . . . . . . . . . . . . . 17 ⊢ ⟨𝑓, 𝑦⟩ ∈ V
31	30	elfix 34875	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑓, 𝑦⟩ ∈ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)) ↔ ⟨𝑓, 𝑦⟩(^◡Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩)
32	30, 30	brco 5871	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑓, 𝑦⟩(^◡Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ ∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥^◡Apply⟨𝑓, 𝑦⟩))
33		ancom 462	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥^◡Apply⟨𝑓, 𝑦⟩) ↔ (𝑥^◡Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
34	5, 30	brcnv 5883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥^◡Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
35	3, 17, 5	brapply 34910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑓, 𝑦⟩Apply𝑥 ↔ 𝑥 = (𝑓‘𝑦))
36	34, 35	bitri 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥^◡Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓‘𝑦))
37	36	anbi1i 625	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥^◡Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ (𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
38	33, 37	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥^◡Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
39	38	exbii 1851	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥^◡Apply⟨𝑓, 𝑦⟩) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
40		fvex 6905	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓‘𝑦) ∈ V
41		breq2 5153	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑦) → (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦)))
42	40, 41	ceqsexv 3526	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦))
43	39, 42	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥^◡Apply⟨𝑓, 𝑦⟩) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦))
44	30, 40	brco 5871	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦) ↔ ∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
45	3, 17, 5	brrestrict 34921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑓, 𝑦⟩Restrict𝑥 ↔ 𝑥 = (𝑓 ↾ 𝑦))
46	45	anbi1i 625	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
47	46	exbii 1851	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ ∃𝑥(𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
48	3	resex 6030	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ↾ 𝑦) ∈ V
49		breq1 5152	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓 ↾ 𝑦) → (𝑥FullFun𝐹(𝑓‘𝑦) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦)))
50	48, 49	ceqsexv 3526	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦))
51	47, 50	bitri 275	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦))
52	48, 40	brfullfun 34920	. . . . . . . . . . . . . . . . . 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 1851	. . . . . . . . . . 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 3072	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ dom 𝑓 ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
62		rexnal 3101	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ dom 𝑓 ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ¬ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
63	60, 61, 62	3bitr2ri 300	. . . . . . . . 9 ⊢ (¬ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ 𝑓 ∈ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))))
64	63	con1bii 357	. . . . . . . 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 470	. . . . . . 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 3323	. . . . . . . . 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 3526	. . . . . 6 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
73		df-fn 6547	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
74		eqcom 2740	. . . . . . . . . . 11 ⊢ (dom 𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓)
75	74	anbi2i 624	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (Fun 𝑓 ∧ 𝑥 = dom 𝑓))
76		ancom 462	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ 𝑥 = dom 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
77	73, 75, 76	3bitri 297	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
78	77	anbi1i 625	. . . . . . . 8 ⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
79		an12 644	. . . . . . . 8 ⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
80		anass 470	. . . . . . . 8 ⊢ (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))))
81	78, 79, 80	3bitr3ri 302	. . . . . . 7 ⊢ ((𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
82	81	exbii 1851	. . . . . 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 3959	. . . . 5 ⊢ (𝑓 ∈ (( Funs ∩ (^◡Domain “ On)) ∖ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (𝑓 ∈ ( Funs ∩ (^◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))))
85		df-rex 3072	. . . . 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 4922	. 2 ⊢ ∪ (( Funs ∩ (^◡Domain “ On)) ∖ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
89	1, 88	eqtr4i 2764	1 ⊢ recs(𝐹) = ∪ (( Funs ∩ (^◡Domain “ On)) ∖ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 {cab 2710 ∀wral 3062 ∃wrex 3071 ∖ cdif 3946 ∩ cin 3948 ⟨cop 4635 ∪ cuni 4909 class class class wbr 5149 E cep 5580 ^◡ccnv 5676 dom cdm 5677 ↾ cres 5679 “ cima 5680 ∘ ccom 5681 Oncon0 6365 Fun wfun 6538 Fn wfn 6539 ‘cfv 6544 recscrecs 8370 Fix cfix 34807 Funs cfuns 34809 Domaincdomain 34815 Applycapply 34817 FullFuncfullfn 34822 Restrictcrestrict 34823

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-symdif 4243 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-fo 6550 df-fv 6552 df-ov 7412 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-txp 34826 df-pprod 34827 df-bigcup 34830 df-fix 34831 df-funs 34833 df-singleton 34834 df-singles 34835 df-image 34836 df-cart 34837 df-img 34838 df-domain 34839 df-range 34840 df-cap 34842 df-restrict 34843 df-apply 34845 df-funpart 34846 df-fullfun 34847

This theorem is referenced by: (None)

W3C validator