Metamath Proof Explorer

Theorem 0nelop

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

Ref Expression
Assertion 0nelop 
|- -. (/) e. <. A , B >.

Proof

Step Hyp Ref Expression
1 id 
 |-  ( (/) e. <. A , B >. -> (/) e. <. A , B >. )
2 oprcl 
 |-  ( (/) e. <. A , B >. -> ( A e. _V /\ B e. _V ) )
3 dfopg 
 |-  ( ( A e. _V /\ B e. _V ) -> <. A , B >. = { { A } , { A , B } } )
4 2 3 syl 
 |-  ( (/) e. <. A , B >. -> <. A , B >. = { { A } , { A , B } } )
5 1 4 eleqtrd 
 |-  ( (/) e. <. A , B >. -> (/) e. { { A } , { A , B } } )
6 elpri 
 |-  ( (/) e. { { A } , { A , B } } -> ( (/) = { A } \/ (/) = { A , B } ) )
7 5 6 syl 
 |-  ( (/) e. <. A , B >. -> ( (/) = { A } \/ (/) = { A , B } ) )
8 2 simpld 
 |-  ( (/) e. <. A , B >. -> A e. _V )
9 snnzg 
 |-  ( A e. _V -> { A } =/= (/) )
10 8 9 syl 
 |-  ( (/) e. <. A , B >. -> { A } =/= (/) )
11 10 necomd 
 |-  ( (/) e. <. A , B >. -> (/) =/= { A } )
12 prnzg 
 |-  ( A e. _V -> { A , B } =/= (/) )
13 8 12 syl 
 |-  ( (/) e. <. A , B >. -> { A , B } =/= (/) )
14 13 necomd 
 |-  ( (/) e. <. A , B >. -> (/) =/= { A , B } )
15 11 14 jca 
 |-  ( (/) e. <. A , B >. -> ( (/) =/= { A } /\ (/) =/= { A , B } ) )
16 neanior 
 |-  ( ( (/) =/= { A } /\ (/) =/= { A , B } ) <-> -. ( (/) = { A } \/ (/) = { A , B } ) )
17 15 16 sylib 
 |-  ( (/) e. <. A , B >. -> -. ( (/) = { A } \/ (/) = { A , B } ) )
18 7 17 pm2.65i 
 |-  -. (/) e. <. A , B >.