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		snnzg	$$⊢A\in \mathrm{V}\to \left\{A\right\}\ne \varnothing$$
10	8 9	syl	$$⊢\varnothing \in ⟨A,B⟩\to \left\{A\right\}\ne \varnothing$$
11	10	necomd	$$⊢\varnothing \in ⟨A,B⟩\to \varnothing \ne \left\{A\right\}$$
12		prnzg	$$⊢A\in \mathrm{V}\to \left\{A,B\right\}\ne \varnothing$$
13	8 12	syl	$$⊢\varnothing \in ⟨A,B⟩\to \left\{A,B\right\}\ne \varnothing$$
14	13	necomd	$$⊢\varnothing \in ⟨A,B⟩\to \varnothing \ne \left\{A,B\right\}$$
15	11 14	jca	$$⊢\varnothing \in ⟨A,B⟩\to \left(\varnothing \ne \left\{A\right\}\wedge \varnothing \ne \left\{A,B\right\}\right)$$
16		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)$$
17	15 16	sylib	$$⊢\varnothing \in ⟨A,B⟩\to \neg \left(\varnothing =\left\{A\right\}\vee \varnothing =\left\{A,B\right\}\right)$$
18	7 17	pm2.65i	$$⊢\neg \varnothing \in ⟨A,B⟩$$