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 syl6ibr
 |-  ( ( 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 ) ) )