dffun10

		Ref	Expression
	Assertion	dffun10	$⊢ Fun F \leftrightarrow F \subseteq I \circ (V ∖ ((V ∖ I) \circ F))$

Proof

Step	Hyp	Ref	Expression
1		impexp	$⊢ ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow (⟨x, y⟩ \in F \to (⟨x, z⟩ \in F \to y = z))$
2	1	albii	$⊢ \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow \forall z (⟨x, y⟩ \in F \to (⟨x, z⟩ \in F \to y = z))$
3		19.21v	$⊢ \forall z (⟨x, y⟩ \in F \to (⟨x, z⟩ \in F \to y = z)) \leftrightarrow (⟨x, y⟩ \in F \to \forall z (⟨x, z⟩ \in F \to y = z))$
4		vex	$⊢ x \in V$
5		vex	$⊢ y \in V$
6	4 5	opelco	$⊢ ⟨x, y⟩ \in ((V ∖ I) \circ F) \leftrightarrow \exists z (x F z \land z (V ∖ I) y)$
7		df-br	$⊢ x F z \leftrightarrow ⟨x, z⟩ \in F$
8		brv	$⊢ z V y$
9		brdif	$⊢ z (V ∖ I) y \leftrightarrow (z V y \land \neg z I y)$
10	8 9	mpbiran	$⊢ z (V ∖ I) y \leftrightarrow \neg z I y$
11	5	ideq	$⊢ z I y \leftrightarrow z = y$
12		equcom	$⊢ z = y \leftrightarrow y = z$
13	11 12	bitri	$⊢ z I y \leftrightarrow y = z$
14	10 13	xchbinx	$⊢ z (V ∖ I) y \leftrightarrow \neg y = z$
15	7 14	anbi12i	$⊢ (x F z \land z (V ∖ I) y) \leftrightarrow (⟨x, z⟩ \in F \land \neg y = z)$
16	15	exbii	$⊢ \exists z (x F z \land z (V ∖ I) y) \leftrightarrow \exists z (⟨x, z⟩ \in F \land \neg y = z)$
17		exanali	$⊢ \exists z (⟨x, z⟩ \in F \land \neg y = z) \leftrightarrow \neg \forall z (⟨x, z⟩ \in F \to y = z)$
18	6 16 17	3bitri	$⊢ ⟨x, y⟩ \in ((V ∖ I) \circ F) \leftrightarrow \neg \forall z (⟨x, z⟩ \in F \to y = z)$
19	18	con2bii	$⊢ \forall z (⟨x, z⟩ \in F \to y = z) \leftrightarrow \neg ⟨x, y⟩ \in ((V ∖ I) \circ F)$
20		opex	$⊢ ⟨x, y⟩ \in V$
21		eldif	$⊢ ⟨x, y⟩ \in (V ∖ ((V ∖ I) \circ F)) \leftrightarrow (⟨x, y⟩ \in V \land \neg ⟨x, y⟩ \in ((V ∖ I) \circ F))$
22	20 21	mpbiran	$⊢ ⟨x, y⟩ \in (V ∖ ((V ∖ I) \circ F)) \leftrightarrow \neg ⟨x, y⟩ \in ((V ∖ I) \circ F)$
23	19 22	bitr4i	$⊢ \forall z (⟨x, z⟩ \in F \to y = z) \leftrightarrow ⟨x, y⟩ \in (V ∖ ((V ∖ I) \circ F))$
24	23	imbi2i	$⊢ (⟨x, y⟩ \in F \to \forall z (⟨x, z⟩ \in F \to y = z)) \leftrightarrow (⟨x, y⟩ \in F \to ⟨x, y⟩ \in (V ∖ ((V ∖ I) \circ F)))$
25	2 3 24	3bitri	$⊢ \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow (⟨x, y⟩ \in F \to ⟨x, y⟩ \in (V ∖ ((V ∖ I) \circ F)))$
26	25	2albii	$⊢ \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow \forall x \forall y (⟨x, y⟩ \in F \to ⟨x, y⟩ \in (V ∖ ((V ∖ I) \circ F)))$
27		ssrel	$⊢ Rel F \to (F \subseteq V ∖ ((V ∖ I) \circ F) \leftrightarrow \forall x \forall y (⟨x, y⟩ \in F \to ⟨x, y⟩ \in (V ∖ ((V ∖ I) \circ F))))$
28	26 27	bitr4id	$⊢ Rel F \to (\forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow F \subseteq V ∖ ((V ∖ I) \circ F))$
29	28	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 F \subseteq V ∖ ((V ∖ I) \circ F))$
30		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))$
31		sscoid	$⊢ F \subseteq I \circ (V ∖ ((V ∖ I) \circ F)) \leftrightarrow (Rel F \land F \subseteq V ∖ ((V ∖ I) \circ F))$
32	29 30 31	3bitr4i	$⊢ Fun F \leftrightarrow F \subseteq I \circ (V ∖ ((V ∖ I) \circ F))$

Metamath Proof Explorer

Theorem dffun10

Proof