Step |
Hyp |
Ref |
Expression |
1 |
|
notnotb |
|- ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) <-> -. -. E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) ) |
2 |
|
nfv |
|- F/ c ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) |
3 |
|
nfv |
|- F/ d ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) |
4 |
|
nfv |
|- F/ a <. x , y >. = <. c , d >. |
5 |
|
nfv |
|- F/ a c =/= d |
6 |
|
nfsbc1v |
|- F/ a [. c / a ]. [. d / b ]. ph |
7 |
4 5 6
|
nf3an |
|- F/ a ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) |
8 |
|
nfv |
|- F/ b <. x , y >. = <. c , d >. |
9 |
|
nfv |
|- F/ b c =/= d |
10 |
|
nfcv |
|- F/_ b c |
11 |
|
nfsbc1v |
|- F/ b [. d / b ]. ph |
12 |
10 11
|
nfsbcw |
|- F/ b [. c / a ]. [. d / b ]. ph |
13 |
8 9 12
|
nf3an |
|- F/ b ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) |
14 |
|
opeq12 |
|- ( ( a = c /\ b = d ) -> <. a , b >. = <. c , d >. ) |
15 |
14
|
eqeq2d |
|- ( ( a = c /\ b = d ) -> ( <. x , y >. = <. a , b >. <-> <. x , y >. = <. c , d >. ) ) |
16 |
|
simpl |
|- ( ( a = c /\ b = d ) -> a = c ) |
17 |
|
simpr |
|- ( ( a = c /\ b = d ) -> b = d ) |
18 |
16 17
|
neeq12d |
|- ( ( a = c /\ b = d ) -> ( a =/= b <-> c =/= d ) ) |
19 |
|
sbceq1a |
|- ( b = d -> ( ph <-> [. d / b ]. ph ) ) |
20 |
|
sbceq1a |
|- ( a = c -> ( [. d / b ]. ph <-> [. c / a ]. [. d / b ]. ph ) ) |
21 |
19 20
|
sylan9bbr |
|- ( ( a = c /\ b = d ) -> ( ph <-> [. c / a ]. [. d / b ]. ph ) ) |
22 |
15 18 21
|
3anbi123d |
|- ( ( a = c /\ b = d ) -> ( ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) ) |
23 |
2 3 7 13 22
|
cbvex2v |
|- ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) <-> E. c E. d ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) |
24 |
|
vex |
|- x e. _V |
25 |
|
vex |
|- y e. _V |
26 |
24 25
|
opth |
|- ( <. x , y >. = <. c , d >. <-> ( x = c /\ y = d ) ) |
27 |
|
eleq1w |
|- ( y = d -> ( y e. X <-> d e. X ) ) |
28 |
27
|
biimpcd |
|- ( y e. X -> ( y = d -> d e. X ) ) |
29 |
28
|
adantl |
|- ( ( x e. X /\ y e. X ) -> ( y = d -> d e. X ) ) |
30 |
29
|
adantl |
|- ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( y = d -> d e. X ) ) |
31 |
30
|
com12 |
|- ( y = d -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> d e. X ) ) |
32 |
31
|
adantl |
|- ( ( x = c /\ y = d ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> d e. X ) ) |
33 |
26 32
|
sylbi |
|- ( <. x , y >. = <. c , d >. -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> d e. X ) ) |
34 |
33
|
3ad2ant1 |
|- ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> d e. X ) ) |
35 |
34
|
impcom |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> d e. X ) |
36 |
|
eleq1w |
|- ( x = c -> ( x e. X <-> c e. X ) ) |
37 |
36
|
biimpcd |
|- ( x e. X -> ( x = c -> c e. X ) ) |
38 |
37
|
adantr |
|- ( ( x e. X /\ y e. X ) -> ( x = c -> c e. X ) ) |
39 |
38
|
adantl |
|- ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( x = c -> c e. X ) ) |
40 |
39
|
com12 |
|- ( x = c -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> c e. X ) ) |
41 |
40
|
adantr |
|- ( ( x = c /\ y = d ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> c e. X ) ) |
42 |
26 41
|
sylbi |
|- ( <. x , y >. = <. c , d >. -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> c e. X ) ) |
43 |
42
|
3ad2ant1 |
|- ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> c e. X ) ) |
44 |
43
|
impcom |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> c e. X ) |
45 |
|
eqidd |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> <. d , c >. = <. d , c >. ) |
46 |
|
necom |
|- ( c =/= d <-> d =/= c ) |
47 |
46
|
biimpi |
|- ( c =/= d -> d =/= c ) |
48 |
47
|
3ad2ant2 |
|- ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> d =/= c ) |
49 |
48
|
adantl |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> d =/= c ) |
50 |
|
dfich2 |
|- ( [ a <> b ] ph <-> A. c A. d ( [ c / a ] [ d / b ] ph <-> [ d / a ] [ c / b ] ph ) ) |
51 |
|
2sp |
|- ( A. c A. d ( [ c / a ] [ d / b ] ph <-> [ d / a ] [ c / b ] ph ) -> ( [ c / a ] [ d / b ] ph <-> [ d / a ] [ c / b ] ph ) ) |
52 |
|
sbsbc |
|- ( [ d / b ] ph <-> [. d / b ]. ph ) |
53 |
52
|
sbbii |
|- ( [ c / a ] [ d / b ] ph <-> [ c / a ] [. d / b ]. ph ) |
54 |
|
sbsbc |
|- ( [ c / a ] [. d / b ]. ph <-> [. c / a ]. [. d / b ]. ph ) |
55 |
53 54
|
bitri |
|- ( [ c / a ] [ d / b ] ph <-> [. c / a ]. [. d / b ]. ph ) |
56 |
|
sbsbc |
|- ( [ c / b ] ph <-> [. c / b ]. ph ) |
57 |
56
|
sbbii |
|- ( [ d / a ] [ c / b ] ph <-> [ d / a ] [. c / b ]. ph ) |
58 |
|
sbsbc |
|- ( [ d / a ] [. c / b ]. ph <-> [. d / a ]. [. c / b ]. ph ) |
59 |
57 58
|
bitri |
|- ( [ d / a ] [ c / b ] ph <-> [. d / a ]. [. c / b ]. ph ) |
60 |
51 55 59
|
3bitr3g |
|- ( A. c A. d ( [ c / a ] [ d / b ] ph <-> [ d / a ] [ c / b ] ph ) -> ( [. c / a ]. [. d / b ]. ph <-> [. d / a ]. [. c / b ]. ph ) ) |
61 |
60
|
biimpd |
|- ( A. c A. d ( [ c / a ] [ d / b ] ph <-> [ d / a ] [ c / b ] ph ) -> ( [. c / a ]. [. d / b ]. ph -> [. d / a ]. [. c / b ]. ph ) ) |
62 |
50 61
|
sylbi |
|- ( [ a <> b ] ph -> ( [. c / a ]. [. d / b ]. ph -> [. d / a ]. [. c / b ]. ph ) ) |
63 |
62
|
adantr |
|- ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( [. c / a ]. [. d / b ]. ph -> [. d / a ]. [. c / b ]. ph ) ) |
64 |
63
|
com12 |
|- ( [. c / a ]. [. d / b ]. ph -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> [. d / a ]. [. c / b ]. ph ) ) |
65 |
64
|
3ad2ant3 |
|- ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> [. d / a ]. [. c / b ]. ph ) ) |
66 |
65
|
impcom |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> [. d / a ]. [. c / b ]. ph ) |
67 |
|
sbccom |
|- ( [. c / b ]. [. d / a ]. ph <-> [. d / a ]. [. c / b ]. ph ) |
68 |
66 67
|
sylibr |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> [. c / b ]. [. d / a ]. ph ) |
69 |
45 49 68
|
3jca |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> ( <. d , c >. = <. d , c >. /\ d =/= c /\ [. c / b ]. [. d / a ]. ph ) ) |
70 |
|
nfv |
|- F/ b <. d , c >. = <. d , c >. |
71 |
|
nfv |
|- F/ b d =/= c |
72 |
|
nfsbc1v |
|- F/ b [. c / b ]. [. d / a ]. ph |
73 |
70 71 72
|
nf3an |
|- F/ b ( <. d , c >. = <. d , c >. /\ d =/= c /\ [. c / b ]. [. d / a ]. ph ) |
74 |
|
opeq2 |
|- ( b = c -> <. d , b >. = <. d , c >. ) |
75 |
74
|
eqeq2d |
|- ( b = c -> ( <. d , c >. = <. d , b >. <-> <. d , c >. = <. d , c >. ) ) |
76 |
|
neeq2 |
|- ( b = c -> ( d =/= b <-> d =/= c ) ) |
77 |
|
sbceq1a |
|- ( b = c -> ( [. d / a ]. ph <-> [. c / b ]. [. d / a ]. ph ) ) |
78 |
75 76 77
|
3anbi123d |
|- ( b = c -> ( ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) <-> ( <. d , c >. = <. d , c >. /\ d =/= c /\ [. c / b ]. [. d / a ]. ph ) ) ) |
79 |
10 73 78
|
spcegf |
|- ( c e. X -> ( ( <. d , c >. = <. d , c >. /\ d =/= c /\ [. c / b ]. [. d / a ]. ph ) -> E. b ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) ) ) |
80 |
44 69 79
|
sylc |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> E. b ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) ) |
81 |
|
nfcv |
|- F/_ a d |
82 |
|
nfv |
|- F/ a <. d , c >. = <. d , b >. |
83 |
|
nfv |
|- F/ a d =/= b |
84 |
|
nfsbc1v |
|- F/ a [. d / a ]. ph |
85 |
82 83 84
|
nf3an |
|- F/ a ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) |
86 |
85
|
nfex |
|- F/ a E. b ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) |
87 |
|
opeq1 |
|- ( a = d -> <. a , b >. = <. d , b >. ) |
88 |
87
|
eqeq2d |
|- ( a = d -> ( <. d , c >. = <. a , b >. <-> <. d , c >. = <. d , b >. ) ) |
89 |
|
neeq1 |
|- ( a = d -> ( a =/= b <-> d =/= b ) ) |
90 |
|
sbceq1a |
|- ( a = d -> ( ph <-> [. d / a ]. ph ) ) |
91 |
88 89 90
|
3anbi123d |
|- ( a = d -> ( ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) ) ) |
92 |
91
|
exbidv |
|- ( a = d -> ( E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) <-> E. b ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) ) ) |
93 |
81 86 92
|
spcegf |
|- ( d e. X -> ( E. b ( <. d , c >. = <. d , b >. /\ d =/= b /\ [. d / a ]. ph ) -> E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) ) ) |
94 |
35 80 93
|
sylc |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) ) |
95 |
|
vex |
|- d e. _V |
96 |
|
vex |
|- c e. _V |
97 |
95 96
|
opth1 |
|- ( <. d , c >. = <. c , d >. -> d = c ) |
98 |
97
|
equcomd |
|- ( <. d , c >. = <. c , d >. -> c = d ) |
99 |
98
|
necon3ai |
|- ( c =/= d -> -. <. d , c >. = <. c , d >. ) |
100 |
99
|
adantl |
|- ( ( <. x , y >. = <. c , d >. /\ c =/= d ) -> -. <. d , c >. = <. c , d >. ) |
101 |
|
eqeq2 |
|- ( <. x , y >. = <. c , d >. -> ( <. d , c >. = <. x , y >. <-> <. d , c >. = <. c , d >. ) ) |
102 |
101
|
adantr |
|- ( ( <. x , y >. = <. c , d >. /\ c =/= d ) -> ( <. d , c >. = <. x , y >. <-> <. d , c >. = <. c , d >. ) ) |
103 |
100 102
|
mtbird |
|- ( ( <. x , y >. = <. c , d >. /\ c =/= d ) -> -. <. d , c >. = <. x , y >. ) |
104 |
103
|
3adant3 |
|- ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> -. <. d , c >. = <. x , y >. ) |
105 |
104
|
adantl |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> -. <. d , c >. = <. x , y >. ) |
106 |
94 105
|
jcnd |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> -. ( E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , c >. = <. x , y >. ) ) |
107 |
|
opeq1 |
|- ( v = d -> <. v , w >. = <. d , w >. ) |
108 |
107
|
eqeq1d |
|- ( v = d -> ( <. v , w >. = <. a , b >. <-> <. d , w >. = <. a , b >. ) ) |
109 |
108
|
3anbi1d |
|- ( v = d -> ( ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) ) ) |
110 |
109
|
2exbidv |
|- ( v = d -> ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) <-> E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) ) ) |
111 |
107
|
eqeq1d |
|- ( v = d -> ( <. v , w >. = <. x , y >. <-> <. d , w >. = <. x , y >. ) ) |
112 |
110 111
|
imbi12d |
|- ( v = d -> ( ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) <-> ( E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , w >. = <. x , y >. ) ) ) |
113 |
112
|
notbid |
|- ( v = d -> ( -. ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) <-> -. ( E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , w >. = <. x , y >. ) ) ) |
114 |
|
opeq2 |
|- ( w = c -> <. d , w >. = <. d , c >. ) |
115 |
114
|
eqeq1d |
|- ( w = c -> ( <. d , w >. = <. a , b >. <-> <. d , c >. = <. a , b >. ) ) |
116 |
115
|
3anbi1d |
|- ( w = c -> ( ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) ) ) |
117 |
116
|
2exbidv |
|- ( w = c -> ( E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) <-> E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) ) ) |
118 |
114
|
eqeq1d |
|- ( w = c -> ( <. d , w >. = <. x , y >. <-> <. d , c >. = <. x , y >. ) ) |
119 |
117 118
|
imbi12d |
|- ( w = c -> ( ( E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , w >. = <. x , y >. ) <-> ( E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , c >. = <. x , y >. ) ) ) |
120 |
119
|
notbid |
|- ( w = c -> ( -. ( E. a E. b ( <. d , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , w >. = <. x , y >. ) <-> -. ( E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , c >. = <. x , y >. ) ) ) |
121 |
113 120
|
rspc2ev |
|- ( ( d e. X /\ c e. X /\ -. ( E. a E. b ( <. d , c >. = <. a , b >. /\ a =/= b /\ ph ) -> <. d , c >. = <. x , y >. ) ) -> E. v e. X E. w e. X -. ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) |
122 |
35 44 106 121
|
syl3anc |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> E. v e. X E. w e. X -. ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) |
123 |
|
rexnal2 |
|- ( E. v e. X E. w e. X -. ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) <-> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) |
124 |
122 123
|
sylib |
|- ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) ) -> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) |
125 |
124
|
ex |
|- ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
126 |
125
|
exlimdvv |
|- ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( E. c E. d ( <. x , y >. = <. c , d >. /\ c =/= d /\ [. c / a ]. [. d / b ]. ph ) -> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
127 |
23 126
|
syl5bi |
|- ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) -> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
128 |
1 127
|
syl5bir |
|- ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( -. -. E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) -> -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
129 |
128
|
orrd |
|- ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( -. E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) \/ -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
130 |
|
ianor |
|- ( -. ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) <-> ( -. E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) \/ -. A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
131 |
129 130
|
sylibr |
|- ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> -. ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
132 |
131
|
ralrimivva |
|- ( [ a <> b ] ph -> A. x e. X A. y e. X -. ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
133 |
|
ralnex2 |
|- ( A. x e. X A. y e. X -. ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) <-> -. E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
134 |
132 133
|
sylib |
|- ( [ a <> b ] ph -> -. E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
135 |
|
eqeq1 |
|- ( p = <. x , y >. -> ( p = <. a , b >. <-> <. x , y >. = <. a , b >. ) ) |
136 |
135
|
3anbi1d |
|- ( p = <. x , y >. -> ( ( p = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) ) ) |
137 |
136
|
2exbidv |
|- ( p = <. x , y >. -> ( E. a E. b ( p = <. a , b >. /\ a =/= b /\ ph ) <-> E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) ) ) |
138 |
|
eqeq1 |
|- ( p = <. v , w >. -> ( p = <. a , b >. <-> <. v , w >. = <. a , b >. ) ) |
139 |
138
|
3anbi1d |
|- ( p = <. v , w >. -> ( ( p = <. a , b >. /\ a =/= b /\ ph ) <-> ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) ) ) |
140 |
139
|
2exbidv |
|- ( p = <. v , w >. -> ( E. a E. b ( p = <. a , b >. /\ a =/= b /\ ph ) <-> E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) ) ) |
141 |
137 140
|
reuop |
|- ( E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ a =/= b /\ ph ) <-> E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ a =/= b /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ a =/= b /\ ph ) -> <. v , w >. = <. x , y >. ) ) ) |
142 |
134 141
|
sylnibr |
|- ( [ a <> b ] ph -> -. E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ a =/= b /\ ph ) ) |