dfrecs2

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

		Ref	Expression
	Assertion	dfrecs2	$⊢ recs (F) = ⋃ ((𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) ∖ dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))))$

Proof

Step	Hyp	Ref	Expression
1		dfrecs3	$⊢ recs (F) = ⋃ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
2		elin	$⊢ f \in (𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) \leftrightarrow (f \in 𝖥𝗎𝗇𝗌 \land f \in {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On])$
3		vex	$⊢ f \in V$
4	3	elfuns	$⊢ f \in 𝖥𝗎𝗇𝗌 \leftrightarrow Fun f$
5		vex	$⊢ x \in V$
6	5 3	brcnv	$⊢ x {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} f \leftrightarrow f 𝖣𝗈𝗆𝖺𝗂𝗇 x$
7	3 5	brdomain	$⊢ f 𝖣𝗈𝗆𝖺𝗂𝗇 x \leftrightarrow x = dom f$
8	6 7	bitri	$⊢ x {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} f \leftrightarrow x = dom f$
9	8	rexbii	$⊢ \exists x \in On x {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} f \leftrightarrow \exists x \in On x = dom f$
10	3	elima	$⊢ f \in {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On] \leftrightarrow \exists x \in On x {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} f$
11		risset	$⊢ dom f \in On \leftrightarrow \exists x \in On x = dom f$
12	9 10 11	3bitr4i	$⊢ f \in {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On] \leftrightarrow dom f \in On$
13	4 12	anbi12i	$⊢ (f \in 𝖥𝗎𝗇𝗌 \land f \in {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) \leftrightarrow (Fun f \land dom f \in On)$
14	2 13	bitri	$⊢ f \in (𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) \leftrightarrow (Fun f \land dom f \in On)$
15	3	eldm	$⊢ f \in dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))) \leftrightarrow \exists y f ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))) y$
16		brdif	$⊢ f ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))) y \leftrightarrow (f (E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) y \land \neg f 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)) y)$
17		vex	$⊢ y \in V$
18	3 17	brco	$⊢ f (E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) y \leftrightarrow \exists x (f 𝖣𝗈𝗆𝖺𝗂𝗇 x \land x E^{-1} y)$
19	7	anbi1i	$⊢ (f 𝖣𝗈𝗆𝖺𝗂𝗇 x \land x E^{-1} y) \leftrightarrow (x = dom f \land x E^{-1} y)$
20	19	exbii	$⊢ \exists x (f 𝖣𝗈𝗆𝖺𝗂𝗇 x \land x E^{-1} y) \leftrightarrow \exists x (x = dom f \land x E^{-1} y)$
21	3	dmex	$⊢ dom f \in V$
22		breq1	$⊢ x = dom f \to (x E^{-1} y \leftrightarrow dom f E^{-1} y)$
23	21 22	ceqsexv	$⊢ \exists x (x = dom f \land x E^{-1} y) \leftrightarrow dom f E^{-1} y$
24	20 23	bitri	$⊢ \exists x (f 𝖣𝗈𝗆𝖺𝗂𝗇 x \land x E^{-1} y) \leftrightarrow dom f E^{-1} y$
25	21 17	brcnv	$⊢ dom f E^{-1} y \leftrightarrow y E dom f$
26	21	epeli	$⊢ y E dom f \leftrightarrow y \in dom f$
27	25 26	bitri	$⊢ dom f E^{-1} y \leftrightarrow y \in dom f$
28	18 24 27	3bitri	$⊢ f (E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) y \leftrightarrow y \in dom f$
29		df-br	$⊢ f 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)) y \leftrightarrow ⟨f, y⟩ \in 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))$
30		opex	$⊢ ⟨f, y⟩ \in V$
31	30	elfix	$⊢ ⟨f, y⟩ \in 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)) \leftrightarrow ⟨f, y⟩ ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)) ⟨f, y⟩$
32	30 30	brco	$⊢ ⟨f, y⟩ ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)) ⟨f, y⟩ \leftrightarrow \exists x (⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x \land x {𝖠𝗉𝗉𝗅𝗒}^{-1} ⟨f, y⟩)$
33		ancom	$⊢ (⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x \land x {𝖠𝗉𝗉𝗅𝗒}^{-1} ⟨f, y⟩) \leftrightarrow (x {𝖠𝗉𝗉𝗅𝗒}^{-1} ⟨f, y⟩ \land ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x)$
34	5 30	brcnv	$⊢ x {𝖠𝗉𝗉𝗅𝗒}^{-1} ⟨f, y⟩ \leftrightarrow ⟨f, y⟩ 𝖠𝗉𝗉𝗅𝗒 x$
35	3 17 5	brapply	$⊢ ⟨f, y⟩ 𝖠𝗉𝗉𝗅𝗒 x \leftrightarrow x = f (y)$
36	34 35	bitri	$⊢ x {𝖠𝗉𝗉𝗅𝗒}^{-1} ⟨f, y⟩ \leftrightarrow x = f (y)$
37	36	anbi1i	$⊢ (x {𝖠𝗉𝗉𝗅𝗒}^{-1} ⟨f, y⟩ \land ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x) \leftrightarrow (x = f (y) \land ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x)$
38	33 37	bitri	$⊢ (⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x \land x {𝖠𝗉𝗉𝗅𝗒}^{-1} ⟨f, y⟩) \leftrightarrow (x = f (y) \land ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x)$
39	38	exbii	$⊢ \exists x (⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x \land x {𝖠𝗉𝗉𝗅𝗒}^{-1} ⟨f, y⟩) \leftrightarrow \exists x (x = f (y) \land ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x)$
40		fvex	$⊢ f (y) \in V$
41		breq2	$⊢ x = f (y) \to (⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x \leftrightarrow ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) f (y))$
42	40 41	ceqsexv	$⊢ \exists x (x = f (y) \land ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x) \leftrightarrow ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) f (y)$
43	39 42	bitri	$⊢ \exists x (⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) x \land x {𝖠𝗉𝗉𝗅𝗒}^{-1} ⟨f, y⟩) \leftrightarrow ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) f (y)$
44	30 40	brco	$⊢ ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) f (y) \leftrightarrow \exists x (⟨f, y⟩ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 x \land x 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y))$
45	3 17 5	brrestrict	$⊢ ⟨f, y⟩ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 x \leftrightarrow x = {f ↾}_{y}$
46	45	anbi1i	$⊢ (⟨f, y⟩ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 x \land x 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y)) \leftrightarrow (x = {f ↾}_{y} \land x 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y))$
47	46	exbii	$⊢ \exists x (⟨f, y⟩ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 x \land x 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y)) \leftrightarrow \exists x (x = {f ↾}_{y} \land x 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y))$
48	3	resex	$⊢ {f ↾}_{y} \in V$
49		breq1	$⊢ x = {f ↾}_{y} \to (x 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y) \leftrightarrow ({f ↾}_{y}) 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y))$
50	48 49	ceqsexv	$⊢ \exists x (x = {f ↾}_{y} \land x 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y)) \leftrightarrow ({f ↾}_{y}) 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y)$
51	47 50	bitri	$⊢ \exists x (⟨f, y⟩ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 x \land x 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y)) \leftrightarrow ({f ↾}_{y}) 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y)$
52	48 40	brfullfun	$⊢ ({f ↾}_{y}) 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F f (y) \leftrightarrow f (y) = F ({f ↾}_{y})$
53	44 51 52	3bitri	$⊢ ⟨f, y⟩ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍) f (y) \leftrightarrow f (y) = F ({f ↾}_{y})$
54	32 43 53	3bitri	$⊢ ⟨f, y⟩ ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)) ⟨f, y⟩ \leftrightarrow f (y) = F ({f ↾}_{y})$
55	29 31 54	3bitri	$⊢ f 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)) y \leftrightarrow f (y) = F ({f ↾}_{y})$
56	55	notbii	$⊢ \neg f 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)) y \leftrightarrow \neg f (y) = F ({f ↾}_{y})$
57	28 56	anbi12i	$⊢ (f (E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) y \land \neg f 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)) y) \leftrightarrow (y \in dom f \land \neg f (y) = F ({f ↾}_{y}))$
58	16 57	bitri	$⊢ f ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))) y \leftrightarrow (y \in dom f \land \neg f (y) = F ({f ↾}_{y}))$
59	58	exbii	$⊢ \exists y f ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))) y \leftrightarrow \exists y (y \in dom f \land \neg f (y) = F ({f ↾}_{y}))$
60	15 59	bitri	$⊢ f \in dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))) \leftrightarrow \exists y (y \in dom f \land \neg f (y) = F ({f ↾}_{y}))$
61		df-rex	$⊢ \exists y \in dom f \neg f (y) = F ({f ↾}_{y}) \leftrightarrow \exists y (y \in dom f \land \neg f (y) = F ({f ↾}_{y}))$
62		rexnal	$⊢ \exists y \in dom f \neg f (y) = F ({f ↾}_{y}) \leftrightarrow \neg \forall y \in dom f f (y) = F ({f ↾}_{y})$
63	60 61 62	3bitr2ri	$⊢ \neg \forall y \in dom f f (y) = F ({f ↾}_{y}) \leftrightarrow f \in dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)))$
64	63	con1bii	$⊢ \neg f \in dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))) \leftrightarrow \forall y \in dom f f (y) = F ({f ↾}_{y})$
65	14 64	anbi12i	$⊢ (f \in (𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) \land \neg f \in dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)))) \leftrightarrow ((Fun f \land dom f \in On) \land \forall y \in dom f f (y) = F ({f ↾}_{y}))$
66		anass	$⊢ ((Fun f \land dom f \in On) \land \forall y \in dom f f (y) = F ({f ↾}_{y})) \leftrightarrow (Fun f \land (dom f \in On \land \forall y \in dom f f (y) = F ({f ↾}_{y})))$
67	65 66	bitri	$⊢ (f \in (𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) \land \neg f \in dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)))) \leftrightarrow (Fun f \land (dom f \in On \land \forall y \in dom f f (y) = F ({f ↾}_{y})))$
68		eleq1	$⊢ x = dom f \to (x \in On \leftrightarrow dom f \in On)$
69		raleq	$⊢ x = dom f \to (\forall y \in x f (y) = F ({f ↾}_{y}) \leftrightarrow \forall y \in dom f f (y) = F ({f ↾}_{y}))$
70	68 69	anbi12d	$⊢ x = dom f \to ((x \in On \land \forall y \in x f (y) = F ({f ↾}_{y})) \leftrightarrow (dom f \in On \land \forall y \in dom f f (y) = F ({f ↾}_{y})))$
71	70	anbi2d	$⊢ x = dom f \to ((Fun f \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y}))) \leftrightarrow (Fun f \land (dom f \in On \land \forall y \in dom f f (y) = F ({f ↾}_{y}))))$
72	21 71	ceqsexv	$⊢ \exists x (x = dom f \land (Fun f \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y})))) \leftrightarrow (Fun f \land (dom f \in On \land \forall y \in dom f f (y) = F ({f ↾}_{y})))$
73		df-fn	$⊢ f Fn x \leftrightarrow (Fun f \land dom f = x)$
74		eqcom	$⊢ dom f = x \leftrightarrow x = dom f$
75	74	anbi2i	$⊢ (Fun f \land dom f = x) \leftrightarrow (Fun f \land x = dom f)$
76		ancom	$⊢ (Fun f \land x = dom f) \leftrightarrow (x = dom f \land Fun f)$
77	73 75 76	3bitri	$⊢ f Fn x \leftrightarrow (x = dom f \land Fun f)$
78	77	anbi1i	$⊢ (f Fn x \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y}))) \leftrightarrow ((x = dom f \land Fun f) \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y})))$
79		an12	$⊢ (f Fn x \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y}))) \leftrightarrow (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
80		anass	$⊢ ((x = dom f \land Fun f) \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y}))) \leftrightarrow (x = dom f \land (Fun f \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y}))))$
81	78 79 80	3bitr3ri	$⊢ (x = dom f \land (Fun f \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y})))) \leftrightarrow (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
82	81	exbii	$⊢ \exists x (x = dom f \land (Fun f \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y})))) \leftrightarrow \exists x (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
83	67 72 82	3bitr2i	$⊢ (f \in (𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) \land \neg f \in dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)))) \leftrightarrow \exists x (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
84		eldif	$⊢ f \in ((𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) ∖ dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)))) \leftrightarrow (f \in (𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) \land \neg f \in dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))))$
85		df-rex	$⊢ \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})) \leftrightarrow \exists x (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
86	83 84 85	3bitr4i	$⊢ f \in ((𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) ∖ dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)))) \leftrightarrow \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))$
87	86	eqabi	$⊢ (𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) ∖ dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))) = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
88	87	unieqi	$⊢ ⋃ ((𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) ∖ dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍)))) = ⋃ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
89	1 88	eqtr4i	$⊢ recs (F) = ⋃ ((𝖥𝗎𝗇𝗌 \cap {𝖣𝗈𝗆𝖺𝗂𝗇}^{-1} [On]) ∖ dom ((E^{-1} \circ 𝖣𝗈𝗆𝖺𝗂𝗇) ∖ 𝖥𝗂𝗑 ({𝖠𝗉𝗉𝗅𝗒}^{-1} \circ (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F \circ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍))))$

Metamath Proof Explorer

Theorem dfrecs2

Proof