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