Metamath Proof Explorer

Theorem ich2exprop

Description: If the setvar variables are interchangeable in a wff, there is an ordered pair fulfilling the wff iff there is an unordered pair fulfilling the wff. (Contributed by AV, 16-Jul-2023)

Ref Expression
Assertion ich2exprop 
|- ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( E. a E. b ( { A , B } = { a , b } /\ ph ) <-> E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ a A e. X
2 nfv 
 |-  F/ a B e. X
3 nfich1 
 |-  F/ a [ a <> b ] ph
4 1 2 3 nf3an 
 |-  F/ a ( A e. X /\ B e. X /\ [ a <> b ] ph )
5 nfv 
 |-  F/ a <. A , B >. = <. x , y >.
6 nfcv 
 |-  F/_ a y
7 nfsbc1v 
 |-  F/ a [. x / a ]. ph
8 6 7 nfsbcw 
 |-  F/ a [. y / b ]. [. x / a ]. ph
9 5 8 nfan 
 |-  F/ a ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph )
10 9 nfex 
 |-  F/ a E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph )
11 10 nfex 
 |-  F/ a E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph )
12 nfv 
 |-  F/ b A e. X
13 nfv 
 |-  F/ b B e. X
14 nfich2 
 |-  F/ b [ a <> b ] ph
15 12 13 14 nf3an 
 |-  F/ b ( A e. X /\ B e. X /\ [ a <> b ] ph )
16 nfv 
 |-  F/ b <. A , B >. = <. x , y >.
17 nfsbc1v 
 |-  F/ b [. y / b ]. [. x / a ]. ph
18 16 17 nfan 
 |-  F/ b ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph )
19 18 nfex 
 |-  F/ b E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph )
20 19 nfex 
 |-  F/ b E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph )
21 vex 
 |-  a e. _V
22 vex 
 |-  b e. _V
23 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 ) ) ) )
24 21 22 23 mpanr12 
 |-  ( ( A e. X /\ B e. X ) -> ( { A , B } = { a , b } <-> ( ( A = a /\ B = b ) \/ ( A = b /\ B = a ) ) ) )
25 24 3adant3 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( { A , B } = { a , b } <-> ( ( A = a /\ B = b ) \/ ( A = b /\ B = a ) ) ) )
26 or2expropbilem1 
 |-  ( ( A e. X /\ B e. X ) -> ( ( A = a /\ B = b ) -> ( ph -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) ) )
27 26 3adant3 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( ( A = a /\ B = b ) -> ( ph -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) ) )
28 ichcom 
 |-  ( [ a <> b ] ph <-> [ b <> a ] ph )
29 28 biimpi 
 |-  ( [ a <> b ] ph -> [ b <> a ] ph )
30 29 3ad2ant3 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> [ b <> a ] ph )
31 30 adantr 
 |-  ( ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) /\ ph ) -> [ b <> a ] ph )
32 22 21 pm3.2i 
 |-  ( b e. _V /\ a e. _V )
33 32 a1i 
 |-  ( ( A = b /\ B = a ) -> ( b e. _V /\ a e. _V ) )
34 31 33 anim12i 
 |-  ( ( ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) /\ ph ) /\ ( A = b /\ B = a ) ) -> ( [ b <> a ] ph /\ ( b e. _V /\ a e. _V ) ) )
35 simpr 
 |-  ( ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) /\ ph ) -> ph )
36 opeq12 
 |-  ( ( A = b /\ B = a ) -> <. A , B >. = <. b , a >. )
37 35 36 anim12ci 
 |-  ( ( ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) /\ ph ) /\ ( A = b /\ B = a ) ) -> ( <. A , B >. = <. b , a >. /\ ph ) )
38 nfv 
 |-  F/ x ( <. A , B >. = <. b , a >. /\ ph )
39 nfv 
 |-  F/ y ( <. A , B >. = <. b , a >. /\ ph )
40 opeq12 
 |-  ( ( x = b /\ y = a ) -> <. x , y >. = <. b , a >. )
41 40 eqeq2d 
 |-  ( ( x = b /\ y = a ) -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. b , a >. ) )
42 41 adantl 
 |-  ( ( [ b <> a ] ph /\ ( x = b /\ y = a ) ) -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. b , a >. ) )
43 dfsbcq 
 |-  ( y = a -> ( [. y / b ]. [. x / a ]. ph <-> [. a / b ]. [. x / a ]. ph ) )
44 43 adantl 
 |-  ( ( x = b /\ y = a ) -> ( [. y / b ]. [. x / a ]. ph <-> [. a / b ]. [. x / a ]. ph ) )
45 44 adantl 
 |-  ( ( [ b <> a ] ph /\ ( x = b /\ y = a ) ) -> ( [. y / b ]. [. x / a ]. ph <-> [. a / b ]. [. x / a ]. ph ) )
46 sbceq1a 
 |-  ( x = b -> ( [. a / b ]. [. x / a ]. ph <-> [. b / x ]. [. a / b ]. [. x / a ]. ph ) )
47 46 adantr 
 |-  ( ( x = b /\ y = a ) -> ( [. a / b ]. [. x / a ]. ph <-> [. b / x ]. [. a / b ]. [. x / a ]. ph ) )
48 df-ich 
 |-  ( [ b <> a ] ph <-> A. b A. a ( [ b / x ] [ a / b ] [ x / a ] ph <-> ph ) )
49 sbsbc 
 |-  ( [ b / x ] [ a / b ] [ x / a ] ph <-> [. b / x ]. [ a / b ] [ x / a ] ph )
50 sbsbc 
 |-  ( [ a / b ] [ x / a ] ph <-> [. a / b ]. [ x / a ] ph )
51 sbsbc 
 |-  ( [ x / a ] ph <-> [. x / a ]. ph )
52 51 sbcbii 
 |-  ( [. a / b ]. [ x / a ] ph <-> [. a / b ]. [. x / a ]. ph )
53 50 52 bitri 
 |-  ( [ a / b ] [ x / a ] ph <-> [. a / b ]. [. x / a ]. ph )
54 53 sbcbii 
 |-  ( [. b / x ]. [ a / b ] [ x / a ] ph <-> [. b / x ]. [. a / b ]. [. x / a ]. ph )
55 49 54 bitri 
 |-  ( [ b / x ] [ a / b ] [ x / a ] ph <-> [. b / x ]. [. a / b ]. [. x / a ]. ph )
56 2sp 
 |-  ( A. b A. a ( [ b / x ] [ a / b ] [ x / a ] ph <-> ph ) -> ( [ b / x ] [ a / b ] [ x / a ] ph <-> ph ) )
57 55 56 bitr3id 
 |-  ( A. b A. a ( [ b / x ] [ a / b ] [ x / a ] ph <-> ph ) -> ( [. b / x ]. [. a / b ]. [. x / a ]. ph <-> ph ) )
58 48 57 sylbi 
 |-  ( [ b <> a ] ph -> ( [. b / x ]. [. a / b ]. [. x / a ]. ph <-> ph ) )
59 47 58 sylan9bbr 
 |-  ( ( [ b <> a ] ph /\ ( x = b /\ y = a ) ) -> ( [. a / b ]. [. x / a ]. ph <-> ph ) )
60 45 59 bitrd 
 |-  ( ( [ b <> a ] ph /\ ( x = b /\ y = a ) ) -> ( [. y / b ]. [. x / a ]. ph <-> ph ) )
61 42 60 anbi12d 
 |-  ( ( [ b <> a ] ph /\ ( x = b /\ y = a ) ) -> ( ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) <-> ( <. A , B >. = <. b , a >. /\ ph ) ) )
62 38 39 61 spc2ed 
 |-  ( ( [ b <> a ] ph /\ ( b e. _V /\ a e. _V ) ) -> ( ( <. A , B >. = <. b , a >. /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) )
63 34 37 62 sylc 
 |-  ( ( ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) /\ ph ) /\ ( A = b /\ B = a ) ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) )
64 63 exp31 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( ph -> ( ( A = b /\ B = a ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) ) )
65 64 com23 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( ( A = b /\ B = a ) -> ( ph -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) ) )
66 27 65 jaod 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( ( ( A = a /\ B = b ) \/ ( A = b /\ B = a ) ) -> ( ph -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) ) )
67 25 66 sylbid 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( { A , B } = { a , b } -> ( ph -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) ) )
68 67 impd 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( ( { A , B } = { a , b } /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) )
69 15 20 68 exlimd 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( E. b ( { A , B } = { a , b } /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) )
70 4 11 69 exlimd 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( E. a E. b ( { A , B } = { a , b } /\ ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) )
71 or2expropbilem2 
 |-  ( E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) <-> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) )
72 70 71 imbitrrdi 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( E. a E. b ( { A , B } = { a , b } /\ ph ) -> E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) ) )
73 oppr 
 |-  ( ( A e. X /\ B e. X ) -> ( <. A , B >. = <. a , b >. -> { A , B } = { a , b } ) )
74 73 anim1d 
 |-  ( ( A e. X /\ B e. X ) -> ( ( <. A , B >. = <. a , b >. /\ ph ) -> ( { A , B } = { a , b } /\ ph ) ) )
75 74 2eximdv 
 |-  ( ( A e. X /\ B e. X ) -> ( E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) -> E. a E. b ( { A , B } = { a , b } /\ ph ) ) )
76 75 3adant3 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) -> E. a E. b ( { A , B } = { a , b } /\ ph ) ) )
77 72 76 impbid 
 |-  ( ( A e. X /\ B e. X /\ [ a <> b ] ph ) -> ( E. a E. b ( { A , B } = { a , b } /\ ph ) <-> E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) ) )