Step |
Hyp |
Ref |
Expression |
0 |
|
cltrr |
|- |
1 |
|
vx |
|- x |
2 |
|
vy |
|- y |
3 |
1
|
cv |
|- x |
4 |
|
cr |
|- RR |
5 |
3 4
|
wcel |
|- x e. RR |
6 |
2
|
cv |
|- y |
7 |
6 4
|
wcel |
|- y e. RR |
8 |
5 7
|
wa |
|- ( x e. RR /\ y e. RR ) |
9 |
|
vz |
|- z |
10 |
|
vw |
|- w |
11 |
9
|
cv |
|- z |
12 |
|
c0r |
|- 0R |
13 |
11 12
|
cop |
|- <. z , 0R >. |
14 |
3 13
|
wceq |
|- x = <. z , 0R >. |
15 |
10
|
cv |
|- w |
16 |
15 12
|
cop |
|- <. w , 0R >. |
17 |
6 16
|
wceq |
|- y = <. w , 0R >. |
18 |
14 17
|
wa |
|- ( x = <. z , 0R >. /\ y = <. w , 0R >. ) |
19 |
|
cltr |
|- |
20 |
11 15 19
|
wbr |
|- z |
21 |
18 20
|
wa |
|- ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z |
22 |
21 10
|
wex |
|- E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z |
23 |
22 9
|
wex |
|- E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z |
24 |
8 23
|
wa |
|- ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z |
25 |
24 1 2
|
copab |
|- { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z |
26 |
0 25
|
wceq |
|- . | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z |