Metamath Proof Explorer

Theorem ordtrest

Description: The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion ordtrest 
|- ( ( R e. PosetRel /\ A e. V ) -> ( ordTop ` ( R i^i ( A X. A ) ) ) C_ ( ( ordTop ` R ) |`t A ) )

Proof

Step Hyp Ref Expression
1 inex1g 
 |-  ( R e. PosetRel -> ( R i^i ( A X. A ) ) e. _V )
2 1 adantr 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( R i^i ( A X. A ) ) e. _V )
3 eqid 
 |-  dom ( R i^i ( A X. A ) ) = dom ( R i^i ( A X. A ) )
4 eqid 
 |-  ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) = ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } )
5 eqid 
 |-  ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) = ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } )
6 3 4 5 ordtval 
 |-  ( ( R i^i ( A X. A ) ) e. _V -> ( ordTop ` ( R i^i ( A X. A ) ) ) = ( topGen ` ( fi ` ( { dom ( R i^i ( A X. A ) ) } u. ( ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) ) ) ) ) )
7 2 6 syl 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( ordTop ` ( R i^i ( A X. A ) ) ) = ( topGen ` ( fi ` ( { dom ( R i^i ( A X. A ) ) } u. ( ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) ) ) ) ) )
8 ordttop 
 |-  ( R e. PosetRel -> ( ordTop ` R ) e. Top )
9 resttop 
 |-  ( ( ( ordTop ` R ) e. Top /\ A e. V ) -> ( ( ordTop ` R ) |`t A ) e. Top )
10 8 9 sylan 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( ( ordTop ` R ) |`t A ) e. Top )
11 eqid 
 |-  dom R = dom R
12 11 psssdm2 
 |-  ( R e. PosetRel -> dom ( R i^i ( A X. A ) ) = ( dom R i^i A ) )
13 12 adantr 
 |-  ( ( R e. PosetRel /\ A e. V ) -> dom ( R i^i ( A X. A ) ) = ( dom R i^i A ) )
14 8 adantr 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( ordTop ` R ) e. Top )
15 simpr 
 |-  ( ( R e. PosetRel /\ A e. V ) -> A e. V )
16 11 ordttopon 
 |-  ( R e. PosetRel -> ( ordTop ` R ) e. ( TopOn ` dom R ) )
17 16 adantr 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( ordTop ` R ) e. ( TopOn ` dom R ) )
18 toponmax 
 |-  ( ( ordTop ` R ) e. ( TopOn ` dom R ) -> dom R e. ( ordTop ` R ) )
19 17 18 syl 
 |-  ( ( R e. PosetRel /\ A e. V ) -> dom R e. ( ordTop ` R ) )
20 elrestr 
 |-  ( ( ( ordTop ` R ) e. Top /\ A e. V /\ dom R e. ( ordTop ` R ) ) -> ( dom R i^i A ) e. ( ( ordTop ` R ) |`t A ) )
21 14 15 19 20 syl3anc 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( dom R i^i A ) e. ( ( ordTop ` R ) |`t A ) )
22 13 21 eqeltrd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> dom ( R i^i ( A X. A ) ) e. ( ( ordTop ` R ) |`t A ) )
23 22 snssd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> { dom ( R i^i ( A X. A ) ) } C_ ( ( ordTop ` R ) |`t A ) )
24 13 rabeqdv 
 |-  ( ( R e. PosetRel /\ A e. V ) -> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } = { y e. ( dom R i^i A ) | -. y ( R i^i ( A X. A ) ) x } )
25 13 24 mpteq12dv 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) = ( x e. ( dom R i^i A ) |-> { y e. ( dom R i^i A ) | -. y ( R i^i ( A X. A ) ) x } ) )
26 25 rneqd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) = ran ( x e. ( dom R i^i A ) |-> { y e. ( dom R i^i A ) | -. y ( R i^i ( A X. A ) ) x } ) )
27 inrab2 
 |-  ( { y e. dom R | -. y R x } i^i A ) = { y e. ( dom R i^i A ) | -. y R x }
28 simpr 
 |-  ( ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) /\ y e. ( dom R i^i A ) ) -> y e. ( dom R i^i A ) )
29 28 elin2d 
 |-  ( ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) /\ y e. ( dom R i^i A ) ) -> y e. A )
30 simpr 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> x e. ( dom R i^i A ) )
31 30 elin2d 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> x e. A )
32 31 adantr 
 |-  ( ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) /\ y e. ( dom R i^i A ) ) -> x e. A )
33 brinxp 
 |-  ( ( y e. A /\ x e. A ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) )
34 29 32 33 syl2anc 
 |-  ( ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) /\ y e. ( dom R i^i A ) ) -> ( y R x <-> y ( R i^i ( A X. A ) ) x ) )
35 34 notbid 
 |-  ( ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) /\ y e. ( dom R i^i A ) ) -> ( -. y R x <-> -. y ( R i^i ( A X. A ) ) x ) )
36 35 rabbidva 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> { y e. ( dom R i^i A ) | -. y R x } = { y e. ( dom R i^i A ) | -. y ( R i^i ( A X. A ) ) x } )
37 27 36 syl5eq 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> ( { y e. dom R | -. y R x } i^i A ) = { y e. ( dom R i^i A ) | -. y ( R i^i ( A X. A ) ) x } )
38 14 adantr 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> ( ordTop ` R ) e. Top )
39 15 adantr 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> A e. V )
40 simpl 
 |-  ( ( R e. PosetRel /\ A e. V ) -> R e. PosetRel )
41 elinel1 
 |-  ( x e. ( dom R i^i A ) -> x e. dom R )
42 11 ordtopn1 
 |-  ( ( R e. PosetRel /\ x e. dom R ) -> { y e. dom R | -. y R x } e. ( ordTop ` R ) )
43 40 41 42 syl2an 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> { y e. dom R | -. y R x } e. ( ordTop ` R ) )
44 elrestr 
 |-  ( ( ( ordTop ` R ) e. Top /\ A e. V /\ { y e. dom R | -. y R x } e. ( ordTop ` R ) ) -> ( { y e. dom R | -. y R x } i^i A ) e. ( ( ordTop ` R ) |`t A ) )
45 38 39 43 44 syl3anc 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> ( { y e. dom R | -. y R x } i^i A ) e. ( ( ordTop ` R ) |`t A ) )
46 37 45 eqeltrrd 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> { y e. ( dom R i^i A ) | -. y ( R i^i ( A X. A ) ) x } e. ( ( ordTop ` R ) |`t A ) )
47 46 fmpttd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( x e. ( dom R i^i A ) |-> { y e. ( dom R i^i A ) | -. y ( R i^i ( A X. A ) ) x } ) : ( dom R i^i A ) --> ( ( ordTop ` R ) |`t A ) )
48 47 frnd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ran ( x e. ( dom R i^i A ) |-> { y e. ( dom R i^i A ) | -. y ( R i^i ( A X. A ) ) x } ) C_ ( ( ordTop ` R ) |`t A ) )
49 26 48 eqsstrd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) C_ ( ( ordTop ` R ) |`t A ) )
50 13 rabeqdv 
 |-  ( ( R e. PosetRel /\ A e. V ) -> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } = { y e. ( dom R i^i A ) | -. x ( R i^i ( A X. A ) ) y } )
51 13 50 mpteq12dv 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) = ( x e. ( dom R i^i A ) |-> { y e. ( dom R i^i A ) | -. x ( R i^i ( A X. A ) ) y } ) )
52 51 rneqd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) = ran ( x e. ( dom R i^i A ) |-> { y e. ( dom R i^i A ) | -. x ( R i^i ( A X. A ) ) y } ) )
53 inrab2 
 |-  ( { y e. dom R | -. x R y } i^i A ) = { y e. ( dom R i^i A ) | -. x R y }
54 brinxp 
 |-  ( ( x e. A /\ y e. A ) -> ( x R y <-> x ( R i^i ( A X. A ) ) y ) )
55 32 29 54 syl2anc 
 |-  ( ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) /\ y e. ( dom R i^i A ) ) -> ( x R y <-> x ( R i^i ( A X. A ) ) y ) )
56 55 notbid 
 |-  ( ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) /\ y e. ( dom R i^i A ) ) -> ( -. x R y <-> -. x ( R i^i ( A X. A ) ) y ) )
57 56 rabbidva 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> { y e. ( dom R i^i A ) | -. x R y } = { y e. ( dom R i^i A ) | -. x ( R i^i ( A X. A ) ) y } )
58 53 57 syl5eq 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> ( { y e. dom R | -. x R y } i^i A ) = { y e. ( dom R i^i A ) | -. x ( R i^i ( A X. A ) ) y } )
59 11 ordtopn2 
 |-  ( ( R e. PosetRel /\ x e. dom R ) -> { y e. dom R | -. x R y } e. ( ordTop ` R ) )
60 40 41 59 syl2an 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> { y e. dom R | -. x R y } e. ( ordTop ` R ) )
61 elrestr 
 |-  ( ( ( ordTop ` R ) e. Top /\ A e. V /\ { y e. dom R | -. x R y } e. ( ordTop ` R ) ) -> ( { y e. dom R | -. x R y } i^i A ) e. ( ( ordTop ` R ) |`t A ) )
62 38 39 60 61 syl3anc 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> ( { y e. dom R | -. x R y } i^i A ) e. ( ( ordTop ` R ) |`t A ) )
63 58 62 eqeltrrd 
 |-  ( ( ( R e. PosetRel /\ A e. V ) /\ x e. ( dom R i^i A ) ) -> { y e. ( dom R i^i A ) | -. x ( R i^i ( A X. A ) ) y } e. ( ( ordTop ` R ) |`t A ) )
64 63 fmpttd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( x e. ( dom R i^i A ) |-> { y e. ( dom R i^i A ) | -. x ( R i^i ( A X. A ) ) y } ) : ( dom R i^i A ) --> ( ( ordTop ` R ) |`t A ) )
65 64 frnd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ran ( x e. ( dom R i^i A ) |-> { y e. ( dom R i^i A ) | -. x ( R i^i ( A X. A ) ) y } ) C_ ( ( ordTop ` R ) |`t A ) )
66 52 65 eqsstrd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) C_ ( ( ordTop ` R ) |`t A ) )
67 49 66 unssd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) ) C_ ( ( ordTop ` R ) |`t A ) )
68 23 67 unssd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( { dom ( R i^i ( A X. A ) ) } u. ( ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) ) ) C_ ( ( ordTop ` R ) |`t A ) )
69 tgfiss 
 |-  ( ( ( ( ordTop ` R ) |`t A ) e. Top /\ ( { dom ( R i^i ( A X. A ) ) } u. ( ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) ) ) C_ ( ( ordTop ` R ) |`t A ) ) -> ( topGen ` ( fi ` ( { dom ( R i^i ( A X. A ) ) } u. ( ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) ) ) ) ) C_ ( ( ordTop ` R ) |`t A ) )
70 10 68 69 syl2anc 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( topGen ` ( fi ` ( { dom ( R i^i ( A X. A ) ) } u. ( ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. y ( R i^i ( A X. A ) ) x } ) u. ran ( x e. dom ( R i^i ( A X. A ) ) |-> { y e. dom ( R i^i ( A X. A ) ) | -. x ( R i^i ( A X. A ) ) y } ) ) ) ) ) C_ ( ( ordTop ` R ) |`t A ) )
71 7 70 eqsstrd 
 |-  ( ( R e. PosetRel /\ A e. V ) -> ( ordTop ` ( R i^i ( A X. A ) ) ) C_ ( ( ordTop ` R ) |`t A ) )