Metamath Proof Explorer


Theorem ordtval

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 X y X | ¬ y R x
ordtval.3 B = ran x X y X | ¬ x R y
Assertion ordtval R V ordTop R = topGen fi X A B

Proof

Step Hyp Ref Expression
1 ordtval.1 X = dom R
2 ordtval.2 A = ran x X y X | ¬ y R x
3 ordtval.3 B = ran x X y X | ¬ x R y
4 elex R V R V
5 dmeq r = R dom r = dom R
6 5 1 eqtr4di r = R dom r = X
7 6 sneqd r = R dom r = X
8 rnun ran x dom r y dom r | ¬ y r x x dom r y dom r | ¬ x r y = ran x dom r y dom r | ¬ y r x ran x dom r y dom r | ¬ x r y
9 breq r = R y r x y R x
10 9 notbid r = R ¬ y r x ¬ y R x
11 6 10 rabeqbidv r = R y dom r | ¬ y r x = y X | ¬ y R x
12 6 11 mpteq12dv r = R x dom r y dom r | ¬ y r x = x X y X | ¬ y R x
13 12 rneqd r = R ran x dom r y dom r | ¬ y r x = ran x X y X | ¬ y R x
14 13 2 eqtr4di r = R ran x dom r y dom r | ¬ y r x = A
15 breq r = R x r y x R y
16 15 notbid r = R ¬ x r y ¬ x R y
17 6 16 rabeqbidv r = R y dom r | ¬ x r y = y X | ¬ x R y
18 6 17 mpteq12dv r = R x dom r y dom r | ¬ x r y = x X y X | ¬ x R y
19 18 rneqd r = R ran x dom r y dom r | ¬ x r y = ran x X y X | ¬ x R y
20 19 3 eqtr4di r = R ran x dom r y dom r | ¬ x r y = B
21 14 20 uneq12d r = R ran x dom r y dom r | ¬ y r x ran x dom r y dom r | ¬ x r y = A B
22 8 21 syl5eq r = R ran x dom r y dom r | ¬ y r x x dom r y dom r | ¬ x r y = A B
23 7 22 uneq12d r = R dom r ran x dom r y dom r | ¬ y r x x dom r y dom r | ¬ x r y = X A B
24 23 fveq2d r = R fi dom r ran x dom r y dom r | ¬ y r x x dom r y dom r | ¬ x r y = fi X A B
25 24 fveq2d r = R topGen fi dom r ran x dom r y dom r | ¬ y r x x dom r y dom r | ¬ x r y = topGen fi X A B
26 df-ordt ordTop = r V topGen fi dom r ran x dom r y dom r | ¬ y r x x dom r y dom r | ¬ x r y
27 fvex topGen fi X A B V
28 25 26 27 fvmpt R V ordTop R = topGen fi X A B
29 4 28 syl R V ordTop R = topGen fi X A B