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 34910

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 8368	. 2 ⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
2		elin 3963	. . . . . . . . 9 ⊢ (𝑓 ∈ ( Funs ∩ (^◡Domain “ On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (^◡Domain “ On)))
3		vex 3478	. . . . . . . . . . 11 ⊢ 𝑓 ∈ V
4	3	elfuns 34875	. . . . . . . . . 10 ⊢ (𝑓 ∈ Funs ↔ Fun 𝑓)
5		vex 3478	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
6	5, 3	brcnv 5880	. . . . . . . . . . . . 13 ⊢ (𝑥^◡Domain𝑓 ↔ 𝑓Domain𝑥)
7	3, 5	brdomain 34893	. . . . . . . . . . . . 13 ⊢ (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓)
8	6, 7	bitri 274	. . . . . . . . . . . 12 ⊢ (𝑥^◡Domain𝑓 ↔ 𝑥 = dom 𝑓)
9	8	rexbii 3094	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ On 𝑥^◡Domain𝑓 ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
10	3	elima 6062	. . . . . . . . . . 11 ⊢ (𝑓 ∈ (^◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥^◡Domain𝑓)
11		risset 3230	. . . . . . . . . . 11 ⊢ (dom 𝑓 ∈ On ↔ ∃𝑥 ∈ On 𝑥 = dom 𝑓)
12	9, 10, 11	3bitr4i 302	. . . . . . . . . 10 ⊢ (𝑓 ∈ (^◡Domain “ On) ↔ dom 𝑓 ∈ On)
13	4, 12	anbi12i 627	. . . . . . . . 9 ⊢ ((𝑓 ∈ Funs ∧ 𝑓 ∈ (^◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
14	2, 13	bitri 274	. . . . . . . 8 ⊢ (𝑓 ∈ ( Funs ∩ (^◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
15	3	eldm 5898	. . . . . . . . . . 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 3478	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
18	3, 17	brco 5868	. . . . . . . . . . . . . . 15 ⊢ (𝑓(^◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥^◡ E 𝑦))
19	7	anbi1i 624	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓Domain𝑥 ∧ 𝑥^◡ E 𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥^◡ E 𝑦))
20	19	exbii 1850	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥^◡ E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥^◡ E 𝑦))
21	3	dmex 7898	. . . . . . . . . . . . . . . . 17 ⊢ dom 𝑓 ∈ V
22		breq1 5150	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = dom 𝑓 → (𝑥^◡ E 𝑦 ↔ dom 𝑓^◡ E 𝑦))
23	21, 22	ceqsexv 3525	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥^◡ E 𝑦) ↔ dom 𝑓^◡ E 𝑦)
24	20, 23	bitri 274	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥^◡ E 𝑦) ↔ dom 𝑓^◡ E 𝑦)
25	21, 17	brcnv 5880	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑓^◡ E 𝑦 ↔ 𝑦 E dom 𝑓)
26	21	epeli 5581	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓)
27	25, 26	bitri 274	. . . . . . . . . . . . . . 15 ⊢ (dom 𝑓^◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓)
28	18, 24, 27	3bitri 296	. . . . . . . . . . . . . 14 ⊢ (𝑓(^◡ E ∘ Domain)𝑦 ↔ 𝑦 ∈ dom 𝑓)
29		df-br 5148	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ⟨𝑓, 𝑦⟩ ∈ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))
30		opex 5463	. . . . . . . . . . . . . . . . 17 ⊢ ⟨𝑓, 𝑦⟩ ∈ V
31	30	elfix 34863	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑓, 𝑦⟩ ∈ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)) ↔ ⟨𝑓, 𝑦⟩(^◡Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩)
32	30, 30	brco 5868	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑓, 𝑦⟩(^◡Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ ∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥^◡Apply⟨𝑓, 𝑦⟩))
33		ancom 461	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥^◡Apply⟨𝑓, 𝑦⟩) ↔ (𝑥^◡Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
34	5, 30	brcnv 5880	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥^◡Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
35	3, 17, 5	brapply 34898	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑓, 𝑦⟩Apply𝑥 ↔ 𝑥 = (𝑓‘𝑦))
36	34, 35	bitri 274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥^◡Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓‘𝑦))
37	36	anbi1i 624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥^◡Apply⟨𝑓, 𝑦⟩ ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ (𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
38	33, 37	bitri 274	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥^◡Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
39	38	exbii 1850	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥^◡Apply⟨𝑓, 𝑦⟩) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥))
40		fvex 6901	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓‘𝑦) ∈ V
41		breq2 5151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑓‘𝑦) → (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦)))
42	40, 41	ceqsexv 3525	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(𝑥 = (𝑓‘𝑦) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦))
43	39, 42	bitri 274	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)𝑥 ∧ 𝑥^◡Apply⟨𝑓, 𝑦⟩) ↔ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦))
44	30, 40	brco 5868	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦) ↔ ∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
45	3, 17, 5	brrestrict 34909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑓, 𝑦⟩Restrict𝑥 ↔ 𝑥 = (𝑓 ↾ 𝑦))
46	45	anbi1i 624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
47	46	exbii 1850	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ ∃𝑥(𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)))
48	3	resex 6027	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ↾ 𝑦) ∈ V
49		breq1 5150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑓 ↾ 𝑦) → (𝑥FullFun𝐹(𝑓‘𝑦) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦)))
50	48, 49	ceqsexv 3525	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(𝑥 = (𝑓 ↾ 𝑦) ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦))
51	47, 50	bitri 274	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(⟨𝑓, 𝑦⟩Restrict𝑥 ∧ 𝑥FullFun𝐹(𝑓‘𝑦)) ↔ (𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦))
52	48, 40	brfullfun 34908	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ↾ 𝑦)FullFun𝐹(𝑓‘𝑦) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
53	44, 51, 52	3bitri 296	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ Restrict)(𝑓‘𝑦) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
54	32, 43, 53	3bitri 296	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑓, 𝑦⟩(^◡Apply ∘ (FullFun𝐹 ∘ Restrict))⟨𝑓, 𝑦⟩ ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
55	29, 31, 54	3bitri 296	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
56	55	notbii 319	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑓 Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦 ↔ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
57	28, 56	anbi12i 627	. . . . . . . . . . . . 13 ⊢ ((𝑓(^◡ E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))𝑦) ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
58	16, 57	bitri 274	. . . . . . . . . . . 12 ⊢ (𝑓((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
59	58	exbii 1850	. . . . . . . . . . 11 ⊢ (∃𝑦 𝑓((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))𝑦 ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
60	15, 59	bitri 274	. . . . . . . . . 10 ⊢ (𝑓 ∈ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
61		df-rex 3071	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ dom 𝑓 ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ∃𝑦(𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
62		rexnal 3100	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ dom 𝑓 ¬ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ¬ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))
63	60, 61, 62	3bitr2ri 299	. . . . . . . . 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 627	. . . . . . 7 ⊢ ((𝑓 ∈ ( Funs ∩ (^◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
66		anass 469	. . . . . . 7 ⊢ (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
67	65, 66	bitri 274	. . . . . 6 ⊢ ((𝑓 ∈ ( Funs ∩ (^◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
68		eleq1 2821	. . . . . . . . 9 ⊢ (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
69		raleq 3322	. . . . . . . . 9 ⊢ (𝑥 = dom 𝑓 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
70	68, 69	anbi12d 631	. . . . . . . 8 ⊢ (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
71	70	anbi2d 629	. . . . . . 7 ⊢ (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))))
72	21, 71	ceqsexv 3525	. . . . . 6 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
73		df-fn 6543	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
74		eqcom 2739	. . . . . . . . . . 11 ⊢ (dom 𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓)
75	74	anbi2i 623	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (Fun 𝑓 ∧ 𝑥 = dom 𝑓))
76		ancom 461	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ 𝑥 = dom 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
77	73, 75, 76	3bitri 296	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
78	77	anbi1i 624	. . . . . . . 8 ⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
79		an12 643	. . . . . . . 8 ⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
80		anass 469	. . . . . . . 8 ⊢ (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))))
81	78, 79, 80	3bitr3ri 301	. . . . . . 7 ⊢ ((𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
82	81	exbii 1850	. . . . . 6 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
83	67, 72, 82	3bitr2i 298	. . . . 5 ⊢ ((𝑓 ∈ ( Funs ∩ (^◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
84		eldif 3957	. . . . 5 ⊢ (𝑓 ∈ (( Funs ∩ (^◡Domain “ On)) ∖ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ (𝑓 ∈ ( Funs ∩ (^◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))))
85		df-rex 3071	. . . . 5 ⊢ (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))))
86	83, 84, 85	3bitr4i 302	. . . 4 ⊢ (𝑓 ∈ (( Funs ∩ (^◡Domain “ On)) ∖ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))
87	86	eqabi 2869	. . 3 ⊢ (( Funs ∩ (^◡Domain “ On)) ∖ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
88	87	unieqi 4920	. 2 ⊢ ∪ (( Funs ∩ (^◡Domain “ On)) ∖ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
89	1, 88	eqtr4i 2763	1 ⊢ recs(𝐹) = ∪ (( Funs ∩ (^◡Domain “ On)) ∖ dom ((^◡ E ∘ Domain) ∖ Fix (^◡Apply ∘ (FullFun𝐹 ∘ Restrict))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ∧ wa 396 = wceq 1541 ∃wex 1781 ∈ wcel 2106 {cab 2709 ∀wral 3061 ∃wrex 3070 ∖ cdif 3944 ∩ cin 3946 ⟨cop 4633 ∪ cuni 4907 class class class wbr 5147 E cep 5578 ^◡ccnv 5674 dom cdm 5675 ↾ cres 5677 “ cima 5678 ∘ ccom 5679 Oncon0 6361 Fun wfun 6534 Fn wfn 6535 ‘cfv 6540 recscrecs 8366 Fix cfix 34795 Funs cfuns 34797 Domaincdomain 34803 Applycapply 34805 FullFuncfullfn 34810 Restrictcrestrict 34811

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-symdif 4241 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-fo 6546 df-fv 6548 df-ov 7408 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-txp 34814 df-pprod 34815 df-bigcup 34818 df-fix 34819 df-funs 34821 df-singleton 34822 df-singles 34823 df-image 34824 df-cart 34825 df-img 34826 df-domain 34827 df-range 34828 df-cap 34830 df-restrict 34831 df-apply 34833 df-funpart 34834 df-fullfun 34835

This theorem is referenced by: (None)

W3C validator