Metamath Proof Explorer

Theorem opthprneg

Description: An unordered pair has the ordered pair property (compare opth ) under certain conditions. Variant of opthpr in closed form. (Contributed by AV, 13-Jun-2022)

Ref Expression
Assertion opthprneg 
|- ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )

Proof

Step Hyp Ref Expression
1 preq12bg 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. _V /\ D e. _V ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
2 1 adantlr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) /\ ( C e. _V /\ D e. _V ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
3 idd 
 |-  ( A =/= D -> ( ( A = C /\ B = D ) -> ( A = C /\ B = D ) ) )
4 df-ne 
 |-  ( A =/= D <-> -. A = D )
5 pm2.21 
 |-  ( -. A = D -> ( A = D -> ( B = C -> ( A = C /\ B = D ) ) ) )
6 4 5 sylbi 
 |-  ( A =/= D -> ( A = D -> ( B = C -> ( A = C /\ B = D ) ) ) )
7 6 impd 
 |-  ( A =/= D -> ( ( A = D /\ B = C ) -> ( A = C /\ B = D ) ) )
8 3 7 jaod 
 |-  ( A =/= D -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) -> ( A = C /\ B = D ) ) )
9 orc 
 |-  ( ( A = C /\ B = D ) -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
10 8 9 impbid1 
 |-  ( A =/= D -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) <-> ( A = C /\ B = D ) ) )
11 10 adantl 
 |-  ( ( A =/= B /\ A =/= D ) -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) <-> ( A = C /\ B = D ) ) )
12 11 ad2antlr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) /\ ( C e. _V /\ D e. _V ) ) -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) <-> ( A = C /\ B = D ) ) )
13 2 12 bitrd 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) /\ ( C e. _V /\ D e. _V ) ) -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )
14 13 expcom 
 |-  ( ( C e. _V /\ D e. _V ) -> ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) ) )
15 ianor 
 |-  ( -. ( C e. _V /\ D e. _V ) <-> ( -. C e. _V \/ -. D e. _V ) )
16 simpl 
 |-  ( ( A =/= B /\ A =/= D ) -> A =/= B )
17 16 anim2i 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) -> ( ( A e. V /\ B e. W ) /\ A =/= B ) )
18 df-3an 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) <-> ( ( A e. V /\ B e. W ) /\ A =/= B ) )
19 17 18 sylibr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) -> ( A e. V /\ B e. W /\ A =/= B ) )
20 prneprprc 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ -. C e. _V ) -> { A , B } =/= { C , D } )
21 19 20 sylan 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) /\ -. C e. _V ) -> { A , B } =/= { C , D } )
22 21 ancoms 
 |-  ( ( -. C e. _V /\ ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) ) -> { A , B } =/= { C , D } )
23 eqneqall 
 |-  ( { A , B } = { C , D } -> ( { A , B } =/= { C , D } -> ( A = C /\ B = D ) ) )
24 22 23 syl5com 
 |-  ( ( -. C e. _V /\ ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) ) -> ( { A , B } = { C , D } -> ( A = C /\ B = D ) ) )
25 prneprprc 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ -. D e. _V ) -> { A , B } =/= { D , C } )
26 19 25 sylan 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) /\ -. D e. _V ) -> { A , B } =/= { D , C } )
27 26 ancoms 
 |-  ( ( -. D e. _V /\ ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) ) -> { A , B } =/= { D , C } )
28 prcom 
 |-  { C , D } = { D , C }
29 28 eqeq2i 
 |-  ( { A , B } = { C , D } <-> { A , B } = { D , C } )
30 eqneqall 
 |-  ( { A , B } = { D , C } -> ( { A , B } =/= { D , C } -> ( A = C /\ B = D ) ) )
31 29 30 sylbi 
 |-  ( { A , B } = { C , D } -> ( { A , B } =/= { D , C } -> ( A = C /\ B = D ) ) )
32 27 31 syl5com 
 |-  ( ( -. D e. _V /\ ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) ) -> ( { A , B } = { C , D } -> ( A = C /\ B = D ) ) )
33 24 32 jaoian 
 |-  ( ( ( -. C e. _V \/ -. D e. _V ) /\ ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) ) -> ( { A , B } = { C , D } -> ( A = C /\ B = D ) ) )
34 preq12 
 |-  ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
35 33 34 impbid1 
 |-  ( ( ( -. C e. _V \/ -. D e. _V ) /\ ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) ) -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )
36 35 ex 
 |-  ( ( -. C e. _V \/ -. D e. _V ) -> ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) ) )
37 15 36 sylbi 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) ) )
38 14 37 pm2.61i 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( A =/= B /\ A =/= D ) ) -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )