Step |
Hyp |
Ref |
Expression |
1 |
|
lerel |
|- Rel <_ |
2 |
|
lerelxr |
|- <_ C_ ( RR* X. RR* ) |
3 |
2
|
brel |
|- ( x <_ y -> ( x e. RR* /\ y e. RR* ) ) |
4 |
3
|
adantr |
|- ( ( x <_ y /\ y <_ z ) -> ( x e. RR* /\ y e. RR* ) ) |
5 |
4
|
simpld |
|- ( ( x <_ y /\ y <_ z ) -> x e. RR* ) |
6 |
4
|
simprd |
|- ( ( x <_ y /\ y <_ z ) -> y e. RR* ) |
7 |
2
|
brel |
|- ( y <_ z -> ( y e. RR* /\ z e. RR* ) ) |
8 |
7
|
simprd |
|- ( y <_ z -> z e. RR* ) |
9 |
8
|
adantl |
|- ( ( x <_ y /\ y <_ z ) -> z e. RR* ) |
10 |
5 6 9
|
3jca |
|- ( ( x <_ y /\ y <_ z ) -> ( x e. RR* /\ y e. RR* /\ z e. RR* ) ) |
11 |
|
xrletr |
|- ( ( x e. RR* /\ y e. RR* /\ z e. RR* ) -> ( ( x <_ y /\ y <_ z ) -> x <_ z ) ) |
12 |
10 11
|
mpcom |
|- ( ( x <_ y /\ y <_ z ) -> x <_ z ) |
13 |
12
|
ax-gen |
|- A. z ( ( x <_ y /\ y <_ z ) -> x <_ z ) |
14 |
13
|
gen2 |
|- A. x A. y A. z ( ( x <_ y /\ y <_ z ) -> x <_ z ) |
15 |
|
cotr |
|- ( ( <_ o. <_ ) C_ <_ <-> A. x A. y A. z ( ( x <_ y /\ y <_ z ) -> x <_ z ) ) |
16 |
14 15
|
mpbir |
|- ( <_ o. <_ ) C_ <_ |
17 |
|
asymref |
|- ( ( <_ i^i `' <_ ) = ( _I |` U. U. <_ ) <-> A. x e. U. U. <_ A. y ( ( x <_ y /\ y <_ x ) <-> x = y ) ) |
18 |
|
simpr |
|- ( ( x e. RR* /\ ( x <_ y /\ y <_ x ) ) -> ( x <_ y /\ y <_ x ) ) |
19 |
2
|
brel |
|- ( y <_ x -> ( y e. RR* /\ x e. RR* ) ) |
20 |
19
|
simpld |
|- ( y <_ x -> y e. RR* ) |
21 |
20
|
adantl |
|- ( ( x <_ y /\ y <_ x ) -> y e. RR* ) |
22 |
|
xrletri3 |
|- ( ( x e. RR* /\ y e. RR* ) -> ( x = y <-> ( x <_ y /\ y <_ x ) ) ) |
23 |
21 22
|
sylan2 |
|- ( ( x e. RR* /\ ( x <_ y /\ y <_ x ) ) -> ( x = y <-> ( x <_ y /\ y <_ x ) ) ) |
24 |
18 23
|
mpbird |
|- ( ( x e. RR* /\ ( x <_ y /\ y <_ x ) ) -> x = y ) |
25 |
24
|
ex |
|- ( x e. RR* -> ( ( x <_ y /\ y <_ x ) -> x = y ) ) |
26 |
|
xrleid |
|- ( x e. RR* -> x <_ x ) |
27 |
26 26
|
jca |
|- ( x e. RR* -> ( x <_ x /\ x <_ x ) ) |
28 |
|
breq2 |
|- ( x = y -> ( x <_ x <-> x <_ y ) ) |
29 |
|
breq1 |
|- ( x = y -> ( x <_ x <-> y <_ x ) ) |
30 |
28 29
|
anbi12d |
|- ( x = y -> ( ( x <_ x /\ x <_ x ) <-> ( x <_ y /\ y <_ x ) ) ) |
31 |
27 30
|
syl5ibcom |
|- ( x e. RR* -> ( x = y -> ( x <_ y /\ y <_ x ) ) ) |
32 |
25 31
|
impbid |
|- ( x e. RR* -> ( ( x <_ y /\ y <_ x ) <-> x = y ) ) |
33 |
32
|
alrimiv |
|- ( x e. RR* -> A. y ( ( x <_ y /\ y <_ x ) <-> x = y ) ) |
34 |
|
lefld |
|- RR* = U. U. <_ |
35 |
34
|
eqcomi |
|- U. U. <_ = RR* |
36 |
33 35
|
eleq2s |
|- ( x e. U. U. <_ -> A. y ( ( x <_ y /\ y <_ x ) <-> x = y ) ) |
37 |
17 36
|
mprgbir |
|- ( <_ i^i `' <_ ) = ( _I |` U. U. <_ ) |
38 |
|
xrex |
|- RR* e. _V |
39 |
38 38
|
xpex |
|- ( RR* X. RR* ) e. _V |
40 |
39 2
|
ssexi |
|- <_ e. _V |
41 |
|
isps |
|- ( <_ e. _V -> ( <_ e. PosetRel <-> ( Rel <_ /\ ( <_ o. <_ ) C_ <_ /\ ( <_ i^i `' <_ ) = ( _I |` U. U. <_ ) ) ) ) |
42 |
40 41
|
ax-mp |
|- ( <_ e. PosetRel <-> ( Rel <_ /\ ( <_ o. <_ ) C_ <_ /\ ( <_ i^i `' <_ ) = ( _I |` U. U. <_ ) ) ) |
43 |
1 16 37 42
|
mpbir3an |
|- <_ e. PosetRel |
44 |
|
xrletri |
|- ( ( x e. RR* /\ y e. RR* ) -> ( x <_ y \/ y <_ x ) ) |
45 |
44
|
rgen2 |
|- A. x e. RR* A. y e. RR* ( x <_ y \/ y <_ x ) |
46 |
|
qfto |
|- ( ( RR* X. RR* ) C_ ( <_ u. `' <_ ) <-> A. x e. RR* A. y e. RR* ( x <_ y \/ y <_ x ) ) |
47 |
45 46
|
mpbir |
|- ( RR* X. RR* ) C_ ( <_ u. `' <_ ) |
48 |
|
ledm |
|- RR* = dom <_ |
49 |
48
|
istsr |
|- ( <_ e. TosetRel <-> ( <_ e. PosetRel /\ ( RR* X. RR* ) C_ ( <_ u. `' <_ ) ) ) |
50 |
43 47 49
|
mpbir2an |
|- <_ e. TosetRel |