Step |
Hyp |
Ref |
Expression |
1 |
|
ltrelre |
|- |
2 |
1
|
brel |
|- ( <. A , 0R >. . -> ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) ) |
3 |
|
opelreal |
|- ( <. A , 0R >. e. RR <-> A e. R. ) |
4 |
|
opelreal |
|- ( <. B , 0R >. e. RR <-> B e. R. ) |
5 |
3 4
|
anbi12i |
|- ( ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) <-> ( A e. R. /\ B e. R. ) ) |
6 |
2 5
|
sylib |
|- ( <. A , 0R >. . -> ( A e. R. /\ B e. R. ) ) |
7 |
|
ltrelsr |
|- |
8 |
7
|
brel |
|- ( A ( A e. R. /\ B e. R. ) ) |
9 |
|
opex |
|- <. A , 0R >. e. _V |
10 |
|
opex |
|- <. B , 0R >. e. _V |
11 |
|
eleq1 |
|- ( x = <. A , 0R >. -> ( x e. RR <-> <. A , 0R >. e. RR ) ) |
12 |
11
|
anbi1d |
|- ( x = <. A , 0R >. -> ( ( x e. RR /\ y e. RR ) <-> ( <. A , 0R >. e. RR /\ y e. RR ) ) ) |
13 |
|
eqeq1 |
|- ( x = <. A , 0R >. -> ( x = <. z , 0R >. <-> <. A , 0R >. = <. z , 0R >. ) ) |
14 |
13
|
anbi1d |
|- ( x = <. A , 0R >. -> ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) <-> ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) ) ) |
15 |
14
|
anbi1d |
|- ( x = <. A , 0R >. -> ( ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z |
16 |
15
|
2exbidv |
|- ( x = <. A , 0R >. -> ( E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z |
17 |
12 16
|
anbi12d |
|- ( x = <. A , 0R >. -> ( ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z ( ( <. A , 0R >. e. RR /\ y e. RR ) /\ E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z |
18 |
|
eleq1 |
|- ( y = <. B , 0R >. -> ( y e. RR <-> <. B , 0R >. e. RR ) ) |
19 |
18
|
anbi2d |
|- ( y = <. B , 0R >. -> ( ( <. A , 0R >. e. RR /\ y e. RR ) <-> ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) ) ) |
20 |
|
eqeq1 |
|- ( y = <. B , 0R >. -> ( y = <. w , 0R >. <-> <. B , 0R >. = <. w , 0R >. ) ) |
21 |
20
|
anbi2d |
|- ( y = <. B , 0R >. -> ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) <-> ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) ) ) |
22 |
21
|
anbi1d |
|- ( y = <. B , 0R >. -> ( ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z |
23 |
22
|
2exbidv |
|- ( y = <. B , 0R >. -> ( E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z |
24 |
19 23
|
anbi12d |
|- ( y = <. B , 0R >. -> ( ( ( <. A , 0R >. e. RR /\ y e. RR ) /\ E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z ( ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) /\ E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z |
25 |
|
df-lt |
|- . | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z |
26 |
9 10 17 24 25
|
brab |
|- ( <. A , 0R >. . <-> ( ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) /\ E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z |
27 |
26
|
baib |
|- ( ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) -> ( <. A , 0R >. . <-> E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z |
28 |
|
vex |
|- z e. _V |
29 |
28
|
eqresr |
|- ( <. z , 0R >. = <. A , 0R >. <-> z = A ) |
30 |
|
eqcom |
|- ( <. A , 0R >. = <. z , 0R >. <-> <. z , 0R >. = <. A , 0R >. ) |
31 |
|
eqcom |
|- ( A = z <-> z = A ) |
32 |
29 30 31
|
3bitr4i |
|- ( <. A , 0R >. = <. z , 0R >. <-> A = z ) |
33 |
|
vex |
|- w e. _V |
34 |
33
|
eqresr |
|- ( <. w , 0R >. = <. B , 0R >. <-> w = B ) |
35 |
|
eqcom |
|- ( <. B , 0R >. = <. w , 0R >. <-> <. w , 0R >. = <. B , 0R >. ) |
36 |
|
eqcom |
|- ( B = w <-> w = B ) |
37 |
34 35 36
|
3bitr4i |
|- ( <. B , 0R >. = <. w , 0R >. <-> B = w ) |
38 |
32 37
|
anbi12i |
|- ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) <-> ( A = z /\ B = w ) ) |
39 |
28 33
|
opth2 |
|- ( <. A , B >. = <. z , w >. <-> ( A = z /\ B = w ) ) |
40 |
38 39
|
bitr4i |
|- ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) <-> <. A , B >. = <. z , w >. ) |
41 |
40
|
anbi1i |
|- ( ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z ( <. A , B >. = <. z , w >. /\ z |
42 |
41
|
2exbii |
|- ( E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z E. z E. w ( <. A , B >. = <. z , w >. /\ z |
43 |
27 42
|
bitrdi |
|- ( ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) -> ( <. A , 0R >. . <-> E. z E. w ( <. A , B >. = <. z , w >. /\ z |
44 |
3 4 43
|
syl2anbr |
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. . <-> E. z E. w ( <. A , B >. = <. z , w >. /\ z |
45 |
|
breq12 |
|- ( ( z = A /\ w = B ) -> ( z A |
46 |
45
|
copsex2g |
|- ( ( A e. R. /\ B e. R. ) -> ( E. z E. w ( <. A , B >. = <. z , w >. /\ z A |
47 |
44 46
|
bitrd |
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. . <-> A |
48 |
6 8 47
|
pm5.21nii |
|- ( <. A , 0R >. . <-> A |