Metamath Proof Explorer

Theorem or2expropbi

Description: If two classes are strictly ordered, there is an ordered pair of both classes fulfilling a wff iff there is an unordered pair of both classes fulfilling the wff. (Contributed by AV, 26-Aug-2023)

Ref Expression
Assertion or2expropbi 
|- ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( E. a E. b ( { A , B } = { a , b } /\ ( a R b /\ ph ) ) <-> E. a E. b ( <. A , B >. = <. a , b >. /\ ( a R b /\ ph ) ) ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ a ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) )
2 nfv 
 |-  F/ a <. A , B >. = <. x , y >.
3 nfcv 
 |-  F/_ a y
4 nfsbc1v 
 |-  F/ a [. x / a ]. ( a R b /\ ph )
5 3 4 nfsbcw 
 |-  F/ a [. y / b ]. [. x / a ]. ( a R b /\ ph )
6 2 5 nfan 
 |-  F/ a ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) )
7 6 nfex 
 |-  F/ a E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) )
8 7 nfex 
 |-  F/ a E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) )
9 nfv 
 |-  F/ b ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) )
10 nfv 
 |-  F/ b <. A , B >. = <. x , y >.
11 nfsbc1v 
 |-  F/ b [. y / b ]. [. x / a ]. ( a R b /\ ph )
12 10 11 nfan 
 |-  F/ b ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) )
13 12 nfex 
 |-  F/ b E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) )
14 13 nfex 
 |-  F/ b E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) )
15 vex 
 |-  a e. _V
16 vex 
 |-  b e. _V
17 preq12bg 
 |-  ( ( ( A e. X /\ B e. X ) /\ ( a e. _V /\ b e. _V ) ) -> ( { A , B } = { a , b } <-> ( ( A = a /\ B = b ) \/ ( A = b /\ B = a ) ) ) )
18 15 16 17 mpanr12 
 |-  ( ( A e. X /\ B e. X ) -> ( { A , B } = { a , b } <-> ( ( A = a /\ B = b ) \/ ( A = b /\ B = a ) ) ) )
19 18 3adant3 
 |-  ( ( A e. X /\ B e. X /\ A R B ) -> ( { A , B } = { a , b } <-> ( ( A = a /\ B = b ) \/ ( A = b /\ B = a ) ) ) )
20 19 adantl 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( { A , B } = { a , b } <-> ( ( A = a /\ B = b ) \/ ( A = b /\ B = a ) ) ) )
21 or2expropbilem1 
 |-  ( ( A e. X /\ B e. X ) -> ( ( A = a /\ B = b ) -> ( ( a R b /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) ) )
22 21 3adant3 
 |-  ( ( A e. X /\ B e. X /\ A R B ) -> ( ( A = a /\ B = b ) -> ( ( a R b /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) ) )
23 22 adantl 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( ( A = a /\ B = b ) -> ( ( a R b /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) ) )
24 breq12 
 |-  ( ( B = a /\ A = b ) -> ( B R A <-> a R b ) )
25 24 ancoms 
 |-  ( ( A = b /\ B = a ) -> ( B R A <-> a R b ) )
26 25 adantl 
 |-  ( ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) /\ ( A = b /\ B = a ) ) -> ( B R A <-> a R b ) )
27 soasym 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> ( A R B -> -. B R A ) )
28 27 ex 
 |-  ( R Or X -> ( ( A e. X /\ B e. X ) -> ( A R B -> -. B R A ) ) )
29 28 adantl 
 |-  ( ( X e. V /\ R Or X ) -> ( ( A e. X /\ B e. X ) -> ( A R B -> -. B R A ) ) )
30 29 expd 
 |-  ( ( X e. V /\ R Or X ) -> ( A e. X -> ( B e. X -> ( A R B -> -. B R A ) ) ) )
31 30 3imp2 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> -. B R A )
32 31 pm2.21d 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( B R A -> ( ph -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) ) )
33 32 adantr 
 |-  ( ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) /\ ( A = b /\ B = a ) ) -> ( B R A -> ( ph -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) ) )
34 26 33 sylbird 
 |-  ( ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) /\ ( A = b /\ B = a ) ) -> ( a R b -> ( ph -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) ) )
35 34 impd 
 |-  ( ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) /\ ( A = b /\ B = a ) ) -> ( ( a R b /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) )
36 35 ex 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( ( A = b /\ B = a ) -> ( ( a R b /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) ) )
37 23 36 jaod 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( ( ( A = a /\ B = b ) \/ ( A = b /\ B = a ) ) -> ( ( a R b /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) ) )
38 20 37 sylbid 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( { A , B } = { a , b } -> ( ( a R b /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) ) )
39 38 impd 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( ( { A , B } = { a , b } /\ ( a R b /\ ph ) ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) )
40 9 14 39 exlimd 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( E. b ( { A , B } = { a , b } /\ ( a R b /\ ph ) ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) )
41 1 8 40 exlimd 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( E. a E. b ( { A , B } = { a , b } /\ ( a R b /\ ph ) ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) ) )
42 or2expropbilem2 
 |-  ( E. a E. b ( <. A , B >. = <. a , b >. /\ ( a R b /\ ph ) ) <-> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ( a R b /\ ph ) ) )
43 41 42 imbitrrdi 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( E. a E. b ( { A , B } = { a , b } /\ ( a R b /\ ph ) ) -> E. a E. b ( <. A , B >. = <. a , b >. /\ ( a R b /\ ph ) ) ) )
44 oppr 
 |-  ( ( A e. X /\ B e. X ) -> ( <. A , B >. = <. a , b >. -> { A , B } = { a , b } ) )
45 44 anim1d 
 |-  ( ( A e. X /\ B e. X ) -> ( ( <. A , B >. = <. a , b >. /\ ( a R b /\ ph ) ) -> ( { A , B } = { a , b } /\ ( a R b /\ ph ) ) ) )
46 45 2eximdv 
 |-  ( ( A e. X /\ B e. X ) -> ( E. a E. b ( <. A , B >. = <. a , b >. /\ ( a R b /\ ph ) ) -> E. a E. b ( { A , B } = { a , b } /\ ( a R b /\ ph ) ) ) )
47 46 3adant3 
 |-  ( ( A e. X /\ B e. X /\ A R B ) -> ( E. a E. b ( <. A , B >. = <. a , b >. /\ ( a R b /\ ph ) ) -> E. a E. b ( { A , B } = { a , b } /\ ( a R b /\ ph ) ) ) )
48 47 adantl 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( E. a E. b ( <. A , B >. = <. a , b >. /\ ( a R b /\ ph ) ) -> E. a E. b ( { A , B } = { a , b } /\ ( a R b /\ ph ) ) ) )
49 43 48 impbid 
 |-  ( ( ( X e. V /\ R Or X ) /\ ( A e. X /\ B e. X /\ A R B ) ) -> ( E. a E. b ( { A , B } = { a , b } /\ ( a R b /\ ph ) ) <-> E. a E. b ( <. A , B >. = <. a , b >. /\ ( a R b /\ ph ) ) ) )