Metamath Proof Explorer

Theorem ordtuni

Description: Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ordtval.1 
|- X = dom R
ordtval.2 
|- A = ran ( x e. X |-> { y e. X | -. y R x } )
ordtval.3 
|- B = ran ( x e. X |-> { y e. X | -. x R y } )
Assertion ordtuni 
|- ( R e. V -> X = U. ( { X } u. ( A u. B ) ) )

Proof

Step Hyp Ref Expression
1 ordtval.1 
 |-  X = dom R
2 ordtval.2 
 |-  A = ran ( x e. X |-> { y e. X | -. y R x } )
3 ordtval.3 
 |-  B = ran ( x e. X |-> { y e. X | -. x R y } )
4 dmexg 
 |-  ( R e. V -> dom R e. _V )
5 1 4 eqeltrid 
 |-  ( R e. V -> X e. _V )
6 unisng 
 |-  ( X e. _V -> U. { X } = X )
7 5 6 syl 
 |-  ( R e. V -> U. { X } = X )
8 7 uneq1d 
 |-  ( R e. V -> ( U. { X } u. U. ( A u. B ) ) = ( X u. U. ( A u. B ) ) )
9 ssrab2 
 |-  { y e. X | -. y R x } C_ X
10 5 adantr 
 |-  ( ( R e. V /\ x e. X ) -> X e. _V )
11 elpw2g 
 |-  ( X e. _V -> ( { y e. X | -. y R x } e. ~P X <-> { y e. X | -. y R x } C_ X ) )
12 10 11 syl 
 |-  ( ( R e. V /\ x e. X ) -> ( { y e. X | -. y R x } e. ~P X <-> { y e. X | -. y R x } C_ X ) )
13 9 12 mpbiri 
 |-  ( ( R e. V /\ x e. X ) -> { y e. X | -. y R x } e. ~P X )
14 13 fmpttd 
 |-  ( R e. V -> ( x e. X |-> { y e. X | -. y R x } ) : X --> ~P X )
15 14 frnd 
 |-  ( R e. V -> ran ( x e. X |-> { y e. X | -. y R x } ) C_ ~P X )
16 2 15 eqsstrid 
 |-  ( R e. V -> A C_ ~P X )
17 ssrab2 
 |-  { y e. X | -. x R y } C_ X
18 elpw2g 
 |-  ( X e. _V -> ( { y e. X | -. x R y } e. ~P X <-> { y e. X | -. x R y } C_ X ) )
19 10 18 syl 
 |-  ( ( R e. V /\ x e. X ) -> ( { y e. X | -. x R y } e. ~P X <-> { y e. X | -. x R y } C_ X ) )
20 17 19 mpbiri 
 |-  ( ( R e. V /\ x e. X ) -> { y e. X | -. x R y } e. ~P X )
21 20 fmpttd 
 |-  ( R e. V -> ( x e. X |-> { y e. X | -. x R y } ) : X --> ~P X )
22 21 frnd 
 |-  ( R e. V -> ran ( x e. X |-> { y e. X | -. x R y } ) C_ ~P X )
23 3 22 eqsstrid 
 |-  ( R e. V -> B C_ ~P X )
24 16 23 unssd 
 |-  ( R e. V -> ( A u. B ) C_ ~P X )
25 sspwuni 
 |-  ( ( A u. B ) C_ ~P X <-> U. ( A u. B ) C_ X )
26 24 25 sylib 
 |-  ( R e. V -> U. ( A u. B ) C_ X )
27 ssequn2 
 |-  ( U. ( A u. B ) C_ X <-> ( X u. U. ( A u. B ) ) = X )
28 26 27 sylib 
 |-  ( R e. V -> ( X u. U. ( A u. B ) ) = X )
29 8 28 eqtr2d 
 |-  ( R e. V -> X = ( U. { X } u. U. ( A u. B ) ) )
30 uniun 
 |-  U. ( { X } u. ( A u. B ) ) = ( U. { X } u. U. ( A u. B ) )
31 29 30 eqtr4di 
 |-  ( R e. V -> X = U. ( { X } u. ( A u. B ) ) )