Theorem 0nelop

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

	Ref	Expression
Assertion	0nelop	⊢ ¬ ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ )
2		oprcl	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
3		dfopg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
4	2 3	syl	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
5	1 4	eleqtrd	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ∅ ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } )
6		elpri	⊢ ( ∅ ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } → ( ∅ = { 𝐴 } ∨ ∅ = { 𝐴 , 𝐵 } ) )
7	5 6	syl	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ( ∅ = { 𝐴 } ∨ ∅ = { 𝐴 , 𝐵 } ) )
8	2	simpld	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → 𝐴 ∈ V )
9		snnzg	⊢ ( 𝐴 ∈ V → { 𝐴 } ≠ ∅ )
10	8 9	syl	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → { 𝐴 } ≠ ∅ )
11	10	necomd	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ∅ ≠ { 𝐴 } )
12		prnzg	⊢ ( 𝐴 ∈ V → { 𝐴 , 𝐵 } ≠ ∅ )
13	8 12	syl	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → { 𝐴 , 𝐵 } ≠ ∅ )
14	13	necomd	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ∅ ≠ { 𝐴 , 𝐵 } )
15	11 14	jca	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ( ∅ ≠ { 𝐴 } ∧ ∅ ≠ { 𝐴 , 𝐵 } ) )
16		neanior	⊢ ( ( ∅ ≠ { 𝐴 } ∧ ∅ ≠ { 𝐴 , 𝐵 } ) ↔ ¬ ( ∅ = { 𝐴 } ∨ ∅ = { 𝐴 , 𝐵 } ) )
17	15 16	sylib	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ¬ ( ∅ = { 𝐴 } ∨ ∅ = { 𝐴 , 𝐵 } ) )
18	7 17	pm2.65i	⊢ ¬ ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩