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 >. |