This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ¬ ∅ ∈ ⟨ 𝐴 , 𝐵 ⟩