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 ) ) )