Metamath Proof Explorer

Theorem ordtprsuni

Description: Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018)

Ref Expression
Hypotheses ordtNEW.b 
|- B = ( Base ` K )
ordtNEW.l 
|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
ordtposval.e 
|- E = ran ( x e. B |-> { y e. B | -. y .<_ x } )
ordtposval.f 
|- F = ran ( x e. B |-> { y e. B | -. x .<_ y } )
Assertion ordtprsuni 
|- ( K e. Proset -> B = U. ( { B } u. ( E u. F ) ) )

Proof

Step Hyp Ref Expression
1 ordtNEW.b 
 |-  B = ( Base ` K )
2 ordtNEW.l 
 |-  .<_ = ( ( le ` K ) i^i ( B X. B ) )
3 ordtposval.e 
 |-  E = ran ( x e. B |-> { y e. B | -. y .<_ x } )
4 ordtposval.f 
 |-  F = ran ( x e. B |-> { y e. B | -. x .<_ y } )
5 1 2 prsdm 
 |-  ( K e. Proset -> dom .<_ = B )
6 5 sneqd 
 |-  ( K e. Proset -> { dom .<_ } = { B } )
7 biidd 
 |-  ( K e. Proset -> ( -. y .<_ x <-> -. y .<_ x ) )
8 5 7 rabeqbidv 
 |-  ( K e. Proset -> { y e. dom .<_ | -. y .<_ x } = { y e. B | -. y .<_ x } )
9 5 8 mpteq12dv 
 |-  ( K e. Proset -> ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) = ( x e. B |-> { y e. B | -. y .<_ x } ) )
10 9 rneqd 
 |-  ( K e. Proset -> ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) = ran ( x e. B |-> { y e. B | -. y .<_ x } ) )
11 biidd 
 |-  ( K e. Proset -> ( -. x .<_ y <-> -. x .<_ y ) )
12 5 11 rabeqbidv 
 |-  ( K e. Proset -> { y e. dom .<_ | -. x .<_ y } = { y e. B | -. x .<_ y } )
13 5 12 mpteq12dv 
 |-  ( K e. Proset -> ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) = ( x e. B |-> { y e. B | -. x .<_ y } ) )
14 13 rneqd 
 |-  ( K e. Proset -> ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) = ran ( x e. B |-> { y e. B | -. x .<_ y } ) )
15 10 14 uneq12d 
 |-  ( K e. Proset -> ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) = ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) )
16 6 15 uneq12d 
 |-  ( K e. Proset -> ( { dom .<_ } u. ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) ) = ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) )
17 16 unieqd 
 |-  ( K e. Proset -> U. ( { dom .<_ } u. ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) ) = U. ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) )
18 fvex 
 |-  ( le ` K ) e. _V
19 18 inex1 
 |-  ( ( le ` K ) i^i ( B X. B ) ) e. _V
20 2 19 eqeltri 
 |-  .<_ e. _V
21 eqid 
 |-  dom .<_ = dom .<_
22 eqid 
 |-  ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) = ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } )
23 eqid 
 |-  ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) = ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } )
24 21 22 23 ordtuni 
 |-  ( .<_ e. _V -> dom .<_ = U. ( { dom .<_ } u. ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) ) )
25 20 24 ax-mp 
 |-  dom .<_ = U. ( { dom .<_ } u. ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) )
26 5 25 eqtr3di 
 |-  ( K e. Proset -> B = U. ( { dom .<_ } u. ( ran ( x e. dom .<_ |-> { y e. dom .<_ | -. y .<_ x } ) u. ran ( x e. dom .<_ |-> { y e. dom .<_ | -. x .<_ y } ) ) ) )
27 3 4 uneq12i 
 |-  ( E u. F ) = ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) )
28 27 a1i 
 |-  ( K e. Proset -> ( E u. F ) = ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) )
29 28 uneq2d 
 |-  ( K e. Proset -> ( { B } u. ( E u. F ) ) = ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) )
30 29 unieqd 
 |-  ( K e. Proset -> U. ( { B } u. ( E u. F ) ) = U. ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) )
31 17 26 30 3eqtr4d 
 |-  ( K e. Proset -> B = U. ( { B } u. ( E u. F ) ) )