0nelop

Description: A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	0nelop	$⊢ \neg \emptyset \in ⟨A, B⟩$

Step	Hyp	Ref	Expression
1		id	$⊢ \emptyset \in ⟨A, B⟩ \to \emptyset \in ⟨A, B⟩$
2		oprcl	$⊢ \emptyset \in ⟨A, B⟩ \to (A \in V \land B \in V)$
3		dfopg	$⊢ (A \in V \land B \in V) \to ⟨A, B⟩ = \{\{A\}, \{A, B\}\}$
4	2 3	syl	$⊢ \emptyset \in ⟨A, B⟩ \to ⟨A, B⟩ = \{\{A\}, \{A, B\}\}$
5	1 4	eleqtrd	$⊢ \emptyset \in ⟨A, B⟩ \to \emptyset \in \{\{A\}, \{A, B\}\}$
6		elpri	$⊢ \emptyset \in \{\{A\}, \{A, B\}\} \to (\emptyset = \{A\} \lor \emptyset = \{A, B\})$
7	5 6	syl	$⊢ \emptyset \in ⟨A, B⟩ \to (\emptyset = \{A\} \lor \emptyset = \{A, B\})$
8	2	simpld	$⊢ \emptyset \in ⟨A, B⟩ \to A \in V$
9	8	snn0d	$⊢ \emptyset \in ⟨A, B⟩ \to \{A\} \neq \emptyset$
10	9	necomd	$⊢ \emptyset \in ⟨A, B⟩ \to \emptyset \neq \{A\}$
11		prnzg	$⊢ A \in V \to \{A, B\} \neq \emptyset$
12	8 11	syl	$⊢ \emptyset \in ⟨A, B⟩ \to \{A, B\} \neq \emptyset$
13	12	necomd	$⊢ \emptyset \in ⟨A, B⟩ \to \emptyset \neq \{A, B\}$
14	10 13	jca	$⊢ \emptyset \in ⟨A, B⟩ \to (\emptyset \neq \{A\} \land \emptyset \neq \{A, B\})$
15		neanior	$⊢ (\emptyset \neq \{A\} \land \emptyset \neq \{A, B\}) \leftrightarrow \neg (\emptyset = \{A\} \lor \emptyset = \{A, B\})$
16	14 15	sylib	$⊢ \emptyset \in ⟨A, B⟩ \to \neg (\emptyset = \{A\} \lor \emptyset = \{A, B\})$
17	7 16	pm2.65i	$⊢ \neg \emptyset \in ⟨A, B⟩$

Metamath Proof Explorer