reldmtpos

Description: Necessary and sufficient condition for dom tpos F to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	reldmtpos	$⊢ Rel dom tpos F \leftrightarrow \neg \emptyset \in dom F$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2	1	eldm	$⊢ \emptyset \in dom F \leftrightarrow \exists y \emptyset F y$
3		brtpos0	$⊢ y \in V \to (\emptyset tpos F y \leftrightarrow \emptyset F y)$
4	3	elv	$⊢ \emptyset tpos F y \leftrightarrow \emptyset F y$
5		0nelrel0	$⊢ Rel dom tpos F \to \neg \emptyset \in dom tpos F$
6		vex	$⊢ y \in V$
7	1 6	breldm	$⊢ \emptyset tpos F y \to \emptyset \in dom tpos F$
8	5 7	nsyl3	$⊢ \emptyset tpos F y \to \neg Rel dom tpos F$
9	4 8	sylbir	$⊢ \emptyset F y \to \neg Rel dom tpos F$
10	9	exlimiv	$⊢ \exists y \emptyset F y \to \neg Rel dom tpos F$
11	2 10	sylbi	$⊢ \emptyset \in dom F \to \neg Rel dom tpos F$
12	11	con2i	$⊢ Rel dom tpos F \to \neg \emptyset \in dom F$
13		vex	$⊢ x \in V$
14	13	eldm	$⊢ x \in dom tpos F \leftrightarrow \exists y x tpos F y$
15		relcnv	$⊢ Rel {dom F}^{-1}$
16		df-rel	$⊢ Rel {dom F}^{-1} \leftrightarrow {dom F}^{-1} \subseteq V \times V$
17	15 16	mpbi	$⊢ {dom F}^{-1} \subseteq V \times V$
18	17	sseli	$⊢ x \in {dom F}^{-1} \to x \in (V \times V)$
19	18	a1i	$⊢ (\neg \emptyset \in dom F \land x tpos F y) \to (x \in {dom F}^{-1} \to x \in (V \times V))$
20		elsni	$⊢ x \in \{\emptyset\} \to x = \emptyset$
21	20	breq1d	$⊢ x \in \{\emptyset\} \to (x tpos F y \leftrightarrow \emptyset tpos F y)$
22	1 6	breldm	$⊢ \emptyset F y \to \emptyset \in dom F$
23	22	pm2.24d	$⊢ \emptyset F y \to (\neg \emptyset \in dom F \to x \in (V \times V))$
24	4 23	sylbi	$⊢ \emptyset tpos F y \to (\neg \emptyset \in dom F \to x \in (V \times V))$
25	21 24	syl6bi	$⊢ x \in \{\emptyset\} \to (x tpos F y \to (\neg \emptyset \in dom F \to x \in (V \times V)))$
26	25	com3l	$⊢ x tpos F y \to (\neg \emptyset \in dom F \to (x \in \{\emptyset\} \to x \in (V \times V)))$
27	26	impcom	$⊢ (\neg \emptyset \in dom F \land x tpos F y) \to (x \in \{\emptyset\} \to x \in (V \times V))$
28		brtpos2	$⊢ y \in V \to (x tpos F y \leftrightarrow (x \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{x\}}^{-1} F y))$
29	6 28	ax-mp	$⊢ x tpos F y \leftrightarrow (x \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{x\}}^{-1} F y)$
30	29	simplbi	$⊢ x tpos F y \to x \in ({dom F}^{-1} \cup \{\emptyset\})$
31		elun	$⊢ x \in ({dom F}^{-1} \cup \{\emptyset\}) \leftrightarrow (x \in {dom F}^{-1} \lor x \in \{\emptyset\})$
32	30 31	sylib	$⊢ x tpos F y \to (x \in {dom F}^{-1} \lor x \in \{\emptyset\})$
33	32	adantl	$⊢ (\neg \emptyset \in dom F \land x tpos F y) \to (x \in {dom F}^{-1} \lor x \in \{\emptyset\})$
34	19 27 33	mpjaod	$⊢ (\neg \emptyset \in dom F \land x tpos F y) \to x \in (V \times V)$
35	34	ex	$⊢ \neg \emptyset \in dom F \to (x tpos F y \to x \in (V \times V))$
36	35	exlimdv	$⊢ \neg \emptyset \in dom F \to (\exists y x tpos F y \to x \in (V \times V))$
37	14 36	biimtrid	$⊢ \neg \emptyset \in dom F \to (x \in dom tpos F \to x \in (V \times V))$
38	37	ssrdv	$⊢ \neg \emptyset \in dom F \to dom tpos F \subseteq V \times V$
39		df-rel	$⊢ Rel dom tpos F \leftrightarrow dom tpos F \subseteq V \times V$
40	38 39	sylibr	$⊢ \neg \emptyset \in dom F \to Rel dom tpos F$
41	12 40	impbii	$⊢ Rel dom tpos F \leftrightarrow \neg \emptyset \in dom F$

Metamath Proof Explorer

Theorem reldmtpos

Proof