elfuns

Description: Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013)

		Ref	Expression
	Hypothesis	elfuns.1	$⊢ F \in V$
	Assertion	elfuns	$⊢ F \in 𝖥𝗎𝗇𝗌 \leftrightarrow Fun F$

Proof

Step	Hyp	Ref	Expression
1		elfuns.1	$⊢ F \in V$
2		elrel	$⊢ (Rel F \land p \in F) \to \exists x \exists y p = ⟨x, y⟩$
3	2	ex	$⊢ Rel F \to (p \in F \to \exists x \exists y p = ⟨x, y⟩)$
4		elrel	$⊢ (Rel F \land q \in F) \to \exists a \exists z q = ⟨a, z⟩$
5	4	ex	$⊢ Rel F \to (q \in F \to \exists a \exists z q = ⟨a, z⟩)$
6	3 5	anim12d	$⊢ Rel F \to ((p \in F \land q \in F) \to (\exists x \exists y p = ⟨x, y⟩ \land \exists a \exists z q = ⟨a, z⟩))$
7	6	adantrd	$⊢ Rel F \to (((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p) \to (\exists x \exists y p = ⟨x, y⟩ \land \exists a \exists z q = ⟨a, z⟩))$
8	7	pm4.71rd	$⊢ Rel F \to (((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p) \leftrightarrow ((\exists x \exists y p = ⟨x, y⟩ \land \exists a \exists z q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)))$
9		19.41vvvv	$⊢ \exists x \exists y \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow (\exists x \exists y \exists a \exists z (p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
10		ee4anv	$⊢ \exists x \exists y \exists a \exists z (p = ⟨x, y⟩ \land q = ⟨a, z⟩) \leftrightarrow (\exists x \exists y p = ⟨x, y⟩ \land \exists a \exists z q = ⟨a, z⟩)$
11	10	anbi1i	$⊢ (\exists x \exists y \exists a \exists z (p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow ((\exists x \exists y p = ⟨x, y⟩ \land \exists a \exists z q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
12	9 11	bitr2i	$⊢ ((\exists x \exists y p = ⟨x, y⟩ \land \exists a \exists z q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \exists x \exists y \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
13	8 12	bitrdi	$⊢ Rel F \to (((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p) \leftrightarrow \exists x \exists y \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)))$
14	13	2exbidv	$⊢ Rel F \to (\exists p \exists q ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p) \leftrightarrow \exists p \exists q \exists x \exists y \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)))$
15		excom13	$⊢ \exists p \exists q \exists x \exists y \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \exists x \exists q \exists p \exists y \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
16		excom13	$⊢ \exists q \exists p \exists y \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \exists y \exists p \exists q \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
17		exrot4	$⊢ \exists p \exists q \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \exists a \exists z \exists p \exists q ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
18		excom	$⊢ \exists a \exists z \exists p \exists q ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \exists z \exists a \exists p \exists q ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
19		df-3an	$⊢ (p = ⟨x, y⟩ \land q = ⟨a, z⟩ \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
20	19	2exbii	$⊢ \exists p \exists q (p = ⟨x, y⟩ \land q = ⟨a, z⟩ \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \exists p \exists q ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
21		opex	$⊢ ⟨x, y⟩ \in V$
22		opex	$⊢ ⟨a, z⟩ \in V$
23		eleq1	$⊢ p = ⟨x, y⟩ \to (p \in F \leftrightarrow ⟨x, y⟩ \in F)$
24	23	anbi1d	$⊢ p = ⟨x, y⟩ \to ((p \in F \land q \in F) \leftrightarrow (⟨x, y⟩ \in F \land q \in F))$
25		breq2	$⊢ p = ⟨x, y⟩ \to (q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p \leftrightarrow q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) ⟨x, y⟩)$
26	24 25	anbi12d	$⊢ p = ⟨x, y⟩ \to (((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p) \leftrightarrow ((⟨x, y⟩ \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) ⟨x, y⟩))$
27		eleq1	$⊢ q = ⟨a, z⟩ \to (q \in F \leftrightarrow ⟨a, z⟩ \in F)$
28	27	anbi2d	$⊢ q = ⟨a, z⟩ \to ((⟨x, y⟩ \in F \land q \in F) \leftrightarrow (⟨x, y⟩ \in F \land ⟨a, z⟩ \in F))$
29		breq1	$⊢ q = ⟨a, z⟩ \to (q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) ⟨x, y⟩ \leftrightarrow ⟨a, z⟩ (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) ⟨x, y⟩)$
30		vex	$⊢ x \in V$
31		vex	$⊢ y \in V$
32	22 30 31	brtxp	$⊢ ⟨a, z⟩ (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) ⟨x, y⟩ \leftrightarrow (⟨a, z⟩ 1^{st} x \land ⟨a, z⟩ ((V ∖ I) \circ 2^{nd}) y)$
33		vex	$⊢ a \in V$
34		vex	$⊢ z \in V$
35	33 34	br1steq	$⊢ ⟨a, z⟩ 1^{st} x \leftrightarrow x = a$
36		equcom	$⊢ x = a \leftrightarrow a = x$
37	35 36	bitri	$⊢ ⟨a, z⟩ 1^{st} x \leftrightarrow a = x$
38	22 31	brco	$⊢ ⟨a, z⟩ ((V ∖ I) \circ 2^{nd}) y \leftrightarrow \exists x (⟨a, z⟩ 2^{nd} x \land x (V ∖ I) y)$
39	33 34	br2ndeq	$⊢ ⟨a, z⟩ 2^{nd} x \leftrightarrow x = z$
40	39	anbi1i	$⊢ (⟨a, z⟩ 2^{nd} x \land x (V ∖ I) y) \leftrightarrow (x = z \land x (V ∖ I) y)$
41	40	exbii	$⊢ \exists x (⟨a, z⟩ 2^{nd} x \land x (V ∖ I) y) \leftrightarrow \exists x (x = z \land x (V ∖ I) y)$
42		breq1	$⊢ x = z \to (x (V ∖ I) y \leftrightarrow z (V ∖ I) y)$
43		brv	$⊢ z V y$
44		brdif	$⊢ z (V ∖ I) y \leftrightarrow (z V y \land \neg z I y)$
45	43 44	mpbiran	$⊢ z (V ∖ I) y \leftrightarrow \neg z I y$
46	31	ideq	$⊢ z I y \leftrightarrow z = y$
47		equcom	$⊢ z = y \leftrightarrow y = z$
48	46 47	bitri	$⊢ z I y \leftrightarrow y = z$
49	48	notbii	$⊢ \neg z I y \leftrightarrow \neg y = z$
50	45 49	bitri	$⊢ z (V ∖ I) y \leftrightarrow \neg y = z$
51	42 50	bitrdi	$⊢ x = z \to (x (V ∖ I) y \leftrightarrow \neg y = z)$
52	51	equsexvw	$⊢ \exists x (x = z \land x (V ∖ I) y) \leftrightarrow \neg y = z$
53	38 41 52	3bitri	$⊢ ⟨a, z⟩ ((V ∖ I) \circ 2^{nd}) y \leftrightarrow \neg y = z$
54	37 53	anbi12i	$⊢ (⟨a, z⟩ 1^{st} x \land ⟨a, z⟩ ((V ∖ I) \circ 2^{nd}) y) \leftrightarrow (a = x \land \neg y = z)$
55	32 54	bitri	$⊢ ⟨a, z⟩ (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) ⟨x, y⟩ \leftrightarrow (a = x \land \neg y = z)$
56	29 55	bitrdi	$⊢ q = ⟨a, z⟩ \to (q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) ⟨x, y⟩ \leftrightarrow (a = x \land \neg y = z))$
57	28 56	anbi12d	$⊢ q = ⟨a, z⟩ \to (((⟨x, y⟩ \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) ⟨x, y⟩) \leftrightarrow ((⟨x, y⟩ \in F \land ⟨a, z⟩ \in F) \land (a = x \land \neg y = z)))$
58		an12	$⊢ ((⟨x, y⟩ \in F \land ⟨a, z⟩ \in F) \land (a = x \land \neg y = z)) \leftrightarrow (a = x \land ((⟨x, y⟩ \in F \land ⟨a, z⟩ \in F) \land \neg y = z))$
59	57 58	bitrdi	$⊢ q = ⟨a, z⟩ \to (((⟨x, y⟩ \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) ⟨x, y⟩) \leftrightarrow (a = x \land ((⟨x, y⟩ \in F \land ⟨a, z⟩ \in F) \land \neg y = z)))$
60	21 22 26 59	ceqsex2v	$⊢ \exists p \exists q (p = ⟨x, y⟩ \land q = ⟨a, z⟩ \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow (a = x \land ((⟨x, y⟩ \in F \land ⟨a, z⟩ \in F) \land \neg y = z))$
61	20 60	bitr3i	$⊢ \exists p \exists q ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow (a = x \land ((⟨x, y⟩ \in F \land ⟨a, z⟩ \in F) \land \neg y = z))$
62	61	exbii	$⊢ \exists a \exists p \exists q ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \exists a (a = x \land ((⟨x, y⟩ \in F \land ⟨a, z⟩ \in F) \land \neg y = z))$
63		opeq1	$⊢ a = x \to ⟨a, z⟩ = ⟨x, z⟩$
64	63	eleq1d	$⊢ a = x \to (⟨a, z⟩ \in F \leftrightarrow ⟨x, z⟩ \in F)$
65	64	anbi2d	$⊢ a = x \to ((⟨x, y⟩ \in F \land ⟨a, z⟩ \in F) \leftrightarrow (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F))$
66	65	anbi1d	$⊢ a = x \to (((⟨x, y⟩ \in F \land ⟨a, z⟩ \in F) \land \neg y = z) \leftrightarrow ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land \neg y = z))$
67	66	equsexvw	$⊢ \exists a (a = x \land ((⟨x, y⟩ \in F \land ⟨a, z⟩ \in F) \land \neg y = z)) \leftrightarrow ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land \neg y = z)$
68	62 67	bitri	$⊢ \exists a \exists p \exists q ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land \neg y = z)$
69	68	exbii	$⊢ \exists z \exists a \exists p \exists q ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \exists z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land \neg y = z)$
70		exanali	$⊢ \exists z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land \neg y = z) \leftrightarrow \neg \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
71	69 70	bitri	$⊢ \exists z \exists a \exists p \exists q ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \neg \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
72	17 18 71	3bitri	$⊢ \exists p \exists q \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \neg \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
73	72	exbii	$⊢ \exists y \exists p \exists q \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \exists y \neg \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
74		exnal	$⊢ \exists y \neg \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow \neg \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
75	16 73 74	3bitri	$⊢ \exists q \exists p \exists y \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \neg \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
76	75	exbii	$⊢ \exists x \exists q \exists p \exists y \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \exists x \neg \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
77		exnal	$⊢ \exists x \neg \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow \neg \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
78	15 76 77	3bitri	$⊢ \exists p \exists q \exists x \exists y \exists a \exists z ((p = ⟨x, y⟩ \land q = ⟨a, z⟩) \land ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)) \leftrightarrow \neg \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
79	14 78	bitrdi	$⊢ Rel F \to (\exists p \exists q ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p) \leftrightarrow \neg \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z))$
80	79	con2bid	$⊢ Rel F \to (\forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow \neg \exists p \exists q ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
81	80	pm5.32i	$⊢ (Rel F \land \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)) \leftrightarrow (Rel F \land \neg \exists p \exists q ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
82		dffun4	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z))$
83		df-funs	$⊢ 𝖥𝗎𝗇𝗌 = 𝒫 (V \times V) ∖ 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1}))$
84	83	eleq2i	$⊢ F \in 𝖥𝗎𝗇𝗌 \leftrightarrow F \in (𝒫 (V \times V) ∖ 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1})))$
85		eldif	$⊢ F \in (𝒫 (V \times V) ∖ 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1}))) \leftrightarrow (F \in 𝒫 (V \times V) \land \neg F \in 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1})))$
86	1	elpw	$⊢ F \in 𝒫 (V \times V) \leftrightarrow F \subseteq V \times V$
87		df-rel	$⊢ Rel F \leftrightarrow F \subseteq V \times V$
88	86 87	bitr4i	$⊢ F \in 𝒫 (V \times V) \leftrightarrow Rel F$
89	1	elfix	$⊢ F \in 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1})) \leftrightarrow F (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1})) F$
90	1 1	coep	$⊢ F (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1})) F \leftrightarrow \exists p \in F F ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1}) p$
91		vex	$⊢ p \in V$
92	1 91	coepr	$⊢ F ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1}) p \leftrightarrow \exists q \in F q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p$
93	92	rexbii	$⊢ \exists p \in F F ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1}) p \leftrightarrow \exists p \in F \exists q \in F q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p$
94	90 93	bitri	$⊢ F (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1})) F \leftrightarrow \exists p \in F \exists q \in F q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p$
95		r2ex	$⊢ \exists p \in F \exists q \in F q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p \leftrightarrow \exists p \exists q ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)$
96	89 94 95	3bitri	$⊢ F \in 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1})) \leftrightarrow \exists p \exists q ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)$
97	96	notbii	$⊢ \neg F \in 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1})) \leftrightarrow \neg \exists p \exists q ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p)$
98	88 97	anbi12i	$⊢ (F \in 𝒫 (V \times V) \land \neg F \in 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1}))) \leftrightarrow (Rel F \land \neg \exists p \exists q ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
99	84 85 98	3bitri	$⊢ F \in 𝖥𝗎𝗇𝗌 \leftrightarrow (Rel F \land \neg \exists p \exists q ((p \in F \land q \in F) \land q (1^{st} \otimes ((V ∖ I) \circ 2^{nd})) p))$
100	81 82 99	3bitr4ri	$⊢ F \in 𝖥𝗎𝗇𝗌 \leftrightarrow Fun F$

Metamath Proof Explorer

Theorem elfuns

Proof