Metamath Proof Explorer


Theorem ordtuni

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

Ref Expression
Hypotheses ordtval.1 X=domR
ordtval.2 A=ranxXyX|¬yRx
ordtval.3 B=ranxXyX|¬xRy
Assertion ordtuni RVX=XAB

Proof

Step Hyp Ref Expression
1 ordtval.1 X=domR
2 ordtval.2 A=ranxXyX|¬yRx
3 ordtval.3 B=ranxXyX|¬xRy
4 dmexg RVdomRV
5 1 4 eqeltrid RVXV
6 unisng XVX=X
7 5 6 syl RVX=X
8 7 uneq1d RVXAB=XAB
9 ssrab2 yX|¬yRxX
10 5 adantr RVxXXV
11 elpw2g XVyX|¬yRx𝒫XyX|¬yRxX
12 10 11 syl RVxXyX|¬yRx𝒫XyX|¬yRxX
13 9 12 mpbiri RVxXyX|¬yRx𝒫X
14 13 fmpttd RVxXyX|¬yRx:X𝒫X
15 14 frnd RVranxXyX|¬yRx𝒫X
16 2 15 eqsstrid RVA𝒫X
17 ssrab2 yX|¬xRyX
18 elpw2g XVyX|¬xRy𝒫XyX|¬xRyX
19 10 18 syl RVxXyX|¬xRy𝒫XyX|¬xRyX
20 17 19 mpbiri RVxXyX|¬xRy𝒫X
21 20 fmpttd RVxXyX|¬xRy:X𝒫X
22 21 frnd RVranxXyX|¬xRy𝒫X
23 3 22 eqsstrid RVB𝒫X
24 16 23 unssd RVAB𝒫X
25 sspwuni AB𝒫XABX
26 24 25 sylib RVABX
27 ssequn2 ABXXAB=X
28 26 27 sylib RVXAB=X
29 8 28 eqtr2d RVX=XAB
30 uniun XAB=XAB
31 29 30 eqtr4di RVX=XAB