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 8 snn0d 
 |-  ( (/) e. <. A , B >. -> { A } =/= (/) )
10 9 necomd 
 |-  ( (/) e. <. A , B >. -> (/) =/= { A } )
11 prnzg 
 |-  ( A e. _V -> { A , B } =/= (/) )
12 8 11 syl 
 |-  ( (/) e. <. A , B >. -> { A , B } =/= (/) )
13 12 necomd 
 |-  ( (/) e. <. A , B >. -> (/) =/= { A , B } )
14 10 13 jca 
 |-  ( (/) e. <. A , B >. -> ( (/) =/= { A } /\ (/) =/= { A , B } ) )
15 neanior 
 |-  ( ( (/) =/= { A } /\ (/) =/= { A , B } ) <-> -. ( (/) = { A } \/ (/) = { A , B } ) )
16 14 15 sylib 
 |-  ( (/) e. <. A , B >. -> -. ( (/) = { A } \/ (/) = { A , B } ) )
17 7 16 pm2.65i 
 |-  -. (/) e. <. A , B >.