Metamath Proof Explorer

Theorem ordtrestNEW

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) (Revised by Thierry Arnoux, 11-Sep-2018)

Ref Expression
Hypotheses ordtNEW.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ordtNEW.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
Assertion ordtrestNEW ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ordtNEW.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ordtNEW.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3 fvex ⊢ ( le ‘ 𝐾 ) ∈ V
4 3 inex1 ⊢ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ∈ V
5 2 4 eqeltri ⊢ ≤ ∈ V
6 5 inex1 ⊢ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∈ V
7 eqid ⊢ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = dom ( ≤ ∩ ( 𝐴 × 𝐴 ) )
8 eqid ⊢ ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) = ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } )
9 eqid ⊢ ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) = ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } )
10 7 8 9 ordtval ⊢ ( ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( topGen ‘ ( fi ‘ ( { dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) } ∪ ( ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ) ) ) )
11 6 10 mp1i ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( topGen ‘ ( fi ‘ ( { dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) } ∪ ( ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ) ) ) )
12 ordttop ⊢ ( ≤ ∈ V → ( ordTop ‘ ≤ ) ∈ Top )
13 5 12 ax-mp ⊢ ( ordTop ‘ ≤ ) ∈ Top
14 fvex ⊢ ( Base ‘ 𝐾 ) ∈ V
15 1 14 eqeltri ⊢ 𝐵 ∈ V
16 15 ssex ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ V )
17 resttop ⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ) → ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ∈ Top )
18 13 16 17 sylancr ⊢ ( 𝐴 ⊆ 𝐵 → ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ∈ Top )
19 18 adantl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ∈ Top )
20 1 ressprs ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐾 ↾s 𝐴 ) ∈ Proset )
21 eqid ⊢ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) )
22 eqid ⊢ ( ( le ‘ ( 𝐾 ↾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) = ( ( le ‘ ( 𝐾 ↾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
23 21 22 prsdm ⊢ ( ( 𝐾 ↾s 𝐴 ) ∈ Proset → dom ( ( le ‘ ( 𝐾 ↾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
24 20 23 syl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → dom ( ( le ‘ ( 𝐾 ↾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
25 eqid ⊢ ( 𝐾 ↾s 𝐴 ) = ( 𝐾 ↾s 𝐴 )
26 25 1 ressbas2 ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
27 fvex ⊢ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ∈ V
28 26 27 eqeltrdi ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ V )
29 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
30 25 29 ressle ⊢ ( 𝐴 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾 ↾s 𝐴 ) ) )
31 28 30 syl ⊢ ( 𝐴 ⊆ 𝐵 → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾 ↾s 𝐴 ) ) )
32 31 adantl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾 ↾s 𝐴 ) ) )
33 26 adantl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
34 33 sqxpeqd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 × 𝐴 ) = ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
35 32 34 ineq12d ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ ( 𝐾 ↾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) )
36 35 dmeqd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → dom ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) = dom ( ( le ‘ ( 𝐾 ↾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) ) )
37 24 36 33 3eqtr4d ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → dom ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
38 1 2 prsss ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) )
39 38 dmeqd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = dom ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) )
40 1 2 prsdm ⊢ ( 𝐾 ∈ Proset → dom ≤ = 𝐵 )
41 40 sseq2d ⊢ ( 𝐾 ∈ Proset → ( 𝐴 ⊆ dom ≤ ↔ 𝐴 ⊆ 𝐵 ) )
42 41 biimpar ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ dom ≤ )
43 sseqin2 ⊢ ( 𝐴 ⊆ dom ≤ ↔ ( dom ≤ ∩ 𝐴 ) = 𝐴 )
44 42 43 sylib ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( dom ≤ ∩ 𝐴 ) = 𝐴 )
45 37 39 44 3eqtr4d ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( dom ≤ ∩ 𝐴 ) )
46 5 12 mp1i ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ordTop ‘ ≤ ) ∈ Top )
47 16 adantl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ V )
48 eqid ⊢ dom ≤ = dom ≤
49 48 ordttopon ⊢ ( ≤ ∈ V → ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ dom ≤ ) )
50 5 49 mp1i ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ dom ≤ ) )
51 toponmax ⊢ ( ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ dom ≤ ) → dom ≤ ∈ ( ordTop ‘ ≤ ) )
52 50 51 syl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → dom ≤ ∈ ( ordTop ‘ ≤ ) )
53 elrestr ⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ∧ dom ≤ ∈ ( ordTop ‘ ≤ ) ) → ( dom ≤ ∩ 𝐴 ) ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
54 46 47 52 53 syl3anc ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( dom ≤ ∩ 𝐴 ) ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
55 45 54 eqeltrd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
56 55 snssd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → { dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) } ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
57 rabeq ⊢ ( dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( dom ≤ ∩ 𝐴 ) → { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } = { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } )
58 45 57 syl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } = { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } )
59 45 58 mpteq12dv ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) = ( 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) )
60 59 rneqd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) = ran ( 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) )
61 inrab2 ⊢ ( { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ∩ 𝐴 ) = { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ≤ 𝑥 }
62 inss2 ⊢ ( dom ≤ ∩ 𝐴 ) ⊆ 𝐴
63 simpr ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ) → 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) )
64 62 63 sseldi ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
65 simpr ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) )
66 62 65 sseldi ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
67 66 adantr ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
68 brinxp ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
69 64 67 68 syl2anc ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ) → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
70 69 notbid ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ) → ( ¬ 𝑦 ≤ 𝑥 ↔ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
71 70 rabbidva ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ≤ 𝑥 } = { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } )
72 61 71 syl5eq ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → ( { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ∩ 𝐴 ) = { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } )
73 5 12 mp1i ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → ( ordTop ‘ ≤ ) ∈ Top )
74 47 adantr ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → 𝐴 ∈ V )
75 simpl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → 𝐾 ∈ Proset )
76 inss1 ⊢ ( dom ≤ ∩ 𝐴 ) ⊆ dom ≤
77 76 sseli ⊢ ( 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) → 𝑥 ∈ dom ≤ )
78 48 ordtopn1 ⊢ ( ( ≤ ∈ V ∧ 𝑥 ∈ dom ≤ ) → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ∈ ( ordTop ‘ ≤ ) )
79 5 78 mpan ⊢ ( 𝑥 ∈ dom ≤ → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ∈ ( ordTop ‘ ≤ ) )
80 79 adantl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ dom ≤ ) → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ∈ ( ordTop ‘ ≤ ) )
81 75 77 80 syl2an ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ∈ ( ordTop ‘ ≤ ) )
82 elrestr ⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ∧ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ∈ ( ordTop ‘ ≤ ) ) → ( { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ∩ 𝐴 ) ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
83 73 74 81 82 syl3anc ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → ( { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ∩ 𝐴 ) ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
84 72 83 eqeltrrd ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
85 84 fmpttd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) : ( dom ≤ ∩ 𝐴 ) ⟶ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
86 85 frnd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ran ( 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
87 60 86 eqsstrd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
88 rabeq ⊢ ( dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( dom ≤ ∩ 𝐴 ) → { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } = { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } )
89 45 88 syl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } = { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } )
90 45 89 mpteq12dv ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) = ( 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) )
91 90 rneqd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) = ran ( 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) )
92 inrab2 ⊢ ( { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ∩ 𝐴 ) = { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ≤ 𝑦 }
93 brinxp ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ) )
94 67 64 93 syl2anc ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ) → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ) )
95 94 notbid ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) ∧ 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ) → ( ¬ 𝑥 ≤ 𝑦 ↔ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ) )
96 95 rabbidva ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ≤ 𝑦 } = { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } )
97 92 96 syl5eq ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → ( { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ∩ 𝐴 ) = { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } )
98 48 ordtopn2 ⊢ ( ( ≤ ∈ V ∧ 𝑥 ∈ dom ≤ ) → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ∈ ( ordTop ‘ ≤ ) )
99 5 98 mpan ⊢ ( 𝑥 ∈ dom ≤ → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ∈ ( ordTop ‘ ≤ ) )
100 99 adantl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ dom ≤ ) → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ∈ ( ordTop ‘ ≤ ) )
101 75 77 100 syl2an ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ∈ ( ordTop ‘ ≤ ) )
102 elrestr ⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ∧ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ∈ ( ordTop ‘ ≤ ) ) → ( { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ∩ 𝐴 ) ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
103 73 74 101 102 syl3anc ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → ( { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ∩ 𝐴 ) ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
104 97 103 eqeltrrd ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ) → { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
105 104 fmpttd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) : ( dom ≤ ∩ 𝐴 ) ⟶ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
106 105 frnd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ran ( 𝑥 ∈ ( dom ≤ ∩ 𝐴 ) ↦ { 𝑦 ∈ ( dom ≤ ∩ 𝐴 ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
107 91 106 eqsstrd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
108 87 107 unssd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
109 56 108 unssd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( { dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) } ∪ ( ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
110 tgfiss ⊢ ( ( ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ∈ Top ∧ ( { dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) } ∪ ( ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ) → ( topGen ‘ ( fi ‘ ( { dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) } ∪ ( ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ) ) ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
111 19 109 110 syl2anc ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( topGen ‘ ( fi ‘ ( { dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) } ∪ ( ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑦 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ↦ { 𝑦 ∈ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑥 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) 𝑦 } ) ) ) ) ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
112 11 111 eqsstrd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )