Description: Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ordtval.1 | |
|
ordtval.2 | |
||
ordtval.3 | |
||
Assertion | ordtuni | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordtval.1 | |
|
2 | ordtval.2 | |
|
3 | ordtval.3 | |
|
4 | dmexg | |
|
5 | 1 4 | eqeltrid | |
6 | unisng | |
|
7 | 5 6 | syl | |
8 | 7 | uneq1d | |
9 | ssrab2 | |
|
10 | 5 | adantr | |
11 | elpw2g | |
|
12 | 10 11 | syl | |
13 | 9 12 | mpbiri | |
14 | 13 | fmpttd | |
15 | 14 | frnd | |
16 | 2 15 | eqsstrid | |
17 | ssrab2 | |
|
18 | elpw2g | |
|
19 | 10 18 | syl | |
20 | 17 19 | mpbiri | |
21 | 20 | fmpttd | |
22 | 21 | frnd | |
23 | 3 22 | eqsstrid | |
24 | 16 23 | unssd | |
25 | sspwuni | |
|
26 | 24 25 | sylib | |
27 | ssequn2 | |
|
28 | 26 27 | sylib | |
29 | 8 28 | eqtr2d | |
30 | uniun | |
|
31 | 29 30 | eqtr4di | |