Metamath Proof Explorer

Theorem poprelb

Description: Equality for unordered pairs with partially ordered elements. (Contributed by AV, 9-Jul-2023)

Ref Expression
Assertion poprelb 
|- ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) /\ ( A R B /\ C R D ) ) -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) /\ ( A R B /\ C R D ) ) -> ( A e. X /\ B e. X ) )
2 an3 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A R B /\ C R D ) ) -> ( Rel R /\ C R D ) )
3 2 3adant2 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) /\ ( A R B /\ C R D ) ) -> ( Rel R /\ C R D ) )
4 brrelex12 
 |-  ( ( Rel R /\ C R D ) -> ( C e. _V /\ D e. _V ) )
5 3 4 syl 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) /\ ( A R B /\ C R D ) ) -> ( C e. _V /\ D e. _V ) )
6 preq12bg 
 |-  ( ( ( A e. X /\ B e. X ) /\ ( C e. _V /\ D e. _V ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
7 1 5 6 syl2anc 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) /\ ( A R B /\ C R D ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
8 idd 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) /\ ( A R B /\ C R D ) ) -> ( ( A = C /\ B = D ) -> ( A = C /\ B = D ) ) )
9 breq12 
 |-  ( ( B = C /\ A = D ) -> ( B R A <-> C R D ) )
10 9 ancoms 
 |-  ( ( A = D /\ B = C ) -> ( B R A <-> C R D ) )
11 10 bicomd 
 |-  ( ( A = D /\ B = C ) -> ( C R D <-> B R A ) )
12 11 anbi2d 
 |-  ( ( A = D /\ B = C ) -> ( ( A R B /\ C R D ) <-> ( A R B /\ B R A ) ) )
13 po2nr 
 |-  ( ( R Po X /\ ( A e. X /\ B e. X ) ) -> -. ( A R B /\ B R A ) )
14 13 adantll 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) ) -> -. ( A R B /\ B R A ) )
15 14 pm2.21d 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) ) -> ( ( A R B /\ B R A ) -> ( A = C /\ B = D ) ) )
16 15 ex 
 |-  ( ( Rel R /\ R Po X ) -> ( ( A e. X /\ B e. X ) -> ( ( A R B /\ B R A ) -> ( A = C /\ B = D ) ) ) )
17 16 com13 
 |-  ( ( A R B /\ B R A ) -> ( ( A e. X /\ B e. X ) -> ( ( Rel R /\ R Po X ) -> ( A = C /\ B = D ) ) ) )
18 12 17 biimtrdi 
 |-  ( ( A = D /\ B = C ) -> ( ( A R B /\ C R D ) -> ( ( A e. X /\ B e. X ) -> ( ( Rel R /\ R Po X ) -> ( A = C /\ B = D ) ) ) ) )
19 18 com23 
 |-  ( ( A = D /\ B = C ) -> ( ( A e. X /\ B e. X ) -> ( ( A R B /\ C R D ) -> ( ( Rel R /\ R Po X ) -> ( A = C /\ B = D ) ) ) ) )
20 19 com14 
 |-  ( ( Rel R /\ R Po X ) -> ( ( A e. X /\ B e. X ) -> ( ( A R B /\ C R D ) -> ( ( A = D /\ B = C ) -> ( A = C /\ B = D ) ) ) ) )
21 20 3imp 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) /\ ( A R B /\ C R D ) ) -> ( ( A = D /\ B = C ) -> ( A = C /\ B = D ) ) )
22 8 21 jaod 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) /\ ( A R B /\ C R D ) ) -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) -> ( A = C /\ B = D ) ) )
23 orc 
 |-  ( ( A = C /\ B = D ) -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
24 22 23 impbid1 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) /\ ( A R B /\ C R D ) ) -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) <-> ( A = C /\ B = D ) ) )
25 7 24 bitrd 
 |-  ( ( ( Rel R /\ R Po X ) /\ ( A e. X /\ B e. X ) /\ ( A R B /\ C R D ) ) -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )