Metamath Proof Explorer


Theorem ordtprsval

Description: Value of the order topology for a proset. (Contributed by Thierry Arnoux, 11-Sep-2015)

Ref Expression
Hypotheses ordtNEW.b B = Base K
ordtNEW.l ˙ = K B × B
ordtposval.e E = ran x B y B | ¬ y ˙ x
ordtposval.f F = ran x B y B | ¬ x ˙ y
Assertion ordtprsval K Proset ordTop ˙ = topGen fi B E F

Proof

Step Hyp Ref Expression
1 ordtNEW.b B = Base K
2 ordtNEW.l ˙ = K B × B
3 ordtposval.e E = ran x B y B | ¬ y ˙ x
4 ordtposval.f F = ran x B y B | ¬ x ˙ y
5 fvex K V
6 5 inex1 K B × B V
7 2 6 eqeltri ˙ V
8 eqid dom ˙ = dom ˙
9 eqid ran x dom ˙ y dom ˙ | ¬ y ˙ x = ran x dom ˙ y dom ˙ | ¬ y ˙ x
10 eqid ran x dom ˙ y dom ˙ | ¬ x ˙ y = ran x dom ˙ y dom ˙ | ¬ x ˙ y
11 8 9 10 ordtval ˙ V ordTop ˙ = topGen fi dom ˙ ran x dom ˙ y dom ˙ | ¬ y ˙ x ran x dom ˙ y dom ˙ | ¬ x ˙ y
12 7 11 ax-mp ordTop ˙ = topGen fi dom ˙ ran x dom ˙ y dom ˙ | ¬ y ˙ x ran x dom ˙ y dom ˙ | ¬ x ˙ y
13 1 2 prsdm K Proset dom ˙ = B
14 13 sneqd K Proset dom ˙ = B
15 13 rabeqdv K Proset y dom ˙ | ¬ y ˙ x = y B | ¬ y ˙ x
16 13 15 mpteq12dv K Proset x dom ˙ y dom ˙ | ¬ y ˙ x = x B y B | ¬ y ˙ x
17 16 rneqd K Proset ran x dom ˙ y dom ˙ | ¬ y ˙ x = ran x B y B | ¬ y ˙ x
18 17 3 eqtr4di K Proset ran x dom ˙ y dom ˙ | ¬ y ˙ x = E
19 13 rabeqdv K Proset y dom ˙ | ¬ x ˙ y = y B | ¬ x ˙ y
20 13 19 mpteq12dv K Proset x dom ˙ y dom ˙ | ¬ x ˙ y = x B y B | ¬ x ˙ y
21 20 rneqd K Proset ran x dom ˙ y dom ˙ | ¬ x ˙ y = ran x B y B | ¬ x ˙ y
22 21 4 eqtr4di K Proset ran x dom ˙ y dom ˙ | ¬ x ˙ y = F
23 18 22 uneq12d K Proset ran x dom ˙ y dom ˙ | ¬ y ˙ x ran x dom ˙ y dom ˙ | ¬ x ˙ y = E F
24 14 23 uneq12d K Proset dom ˙ ran x dom ˙ y dom ˙ | ¬ y ˙ x ran x dom ˙ y dom ˙ | ¬ x ˙ y = B E F
25 24 fveq2d K Proset fi dom ˙ ran x dom ˙ y dom ˙ | ¬ y ˙ x ran x dom ˙ y dom ˙ | ¬ x ˙ y = fi B E F
26 25 fveq2d K Proset topGen fi dom ˙ ran x dom ˙ y dom ˙ | ¬ y ˙ x ran x dom ˙ y dom ˙ | ¬ x ˙ y = topGen fi B E F
27 12 26 syl5eq K Proset ordTop ˙ = topGen fi B E F