Theorem 0nelop

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

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

Proof

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