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	8	snn0d	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → { 𝐴 } ≠ ∅ )
10	9	necomd	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ∅ ≠ { 𝐴 } )
11		prnzg	⊢ ( 𝐴 ∈ V → { 𝐴 , 𝐵 } ≠ ∅ )
12	8 11	syl	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → { 𝐴 , 𝐵 } ≠ ∅ )
13	12	necomd	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ∅ ≠ { 𝐴 , 𝐵 } )
14	10 13	jca	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ( ∅ ≠ { 𝐴 } ∧ ∅ ≠ { 𝐴 , 𝐵 } ) )
15		neanior	⊢ ( ( ∅ ≠ { 𝐴 } ∧ ∅ ≠ { 𝐴 , 𝐵 } ) ↔ ¬ ( ∅ = { 𝐴 } ∨ ∅ = { 𝐴 , 𝐵 } ) )
16	14 15	sylib	⊢ ( ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ¬ ( ∅ = { 𝐴 } ∨ ∅ = { 𝐴 , 𝐵 } ) )
17	7 16	pm2.65i	⊢ ¬ ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩