Metamath Proof Explorer

Theorem ordtcnvNEW

Description: The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015) (Revised by Thierry Arnoux, 13-Sep-2018)

Ref Expression
Hypotheses ordtNEW.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ordtNEW.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
Assertion ordtcnvNEW ( 𝐾 ∈ Proset → ( ordTop ‘ ◡ ≤ ) = ( ordTop ‘ ≤ ) )

Proof

Step Hyp Ref Expression
1 ordtNEW.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ordtNEW.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3 vex ⊢ 𝑦 ∈ V
4 vex ⊢ 𝑥 ∈ V
5 3 4 brcnv ⊢ ( 𝑦 ◡ ≤ 𝑥 ↔ 𝑥 ≤ 𝑦 )
6 5 a1i ⊢ ( 𝐾 ∈ Proset → ( 𝑦 ◡ ≤ 𝑥 ↔ 𝑥 ≤ 𝑦 ) )
7 6 notbid ⊢ ( 𝐾 ∈ Proset → ( ¬ 𝑦 ◡ ≤ 𝑥 ↔ ¬ 𝑥 ≤ 𝑦 ) )
8 7 rabbidv ⊢ ( 𝐾 ∈ Proset → { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
9 8 mpteq2dv ⊢ ( 𝐾 ∈ Proset → ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
10 9 rneqd ⊢ ( 𝐾 ∈ Proset → ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
11 4 3 brcnv ⊢ ( 𝑥 ◡ ≤ 𝑦 ↔ 𝑦 ≤ 𝑥 )
12 11 a1i ⊢ ( 𝐾 ∈ Proset → ( 𝑥 ◡ ≤ 𝑦 ↔ 𝑦 ≤ 𝑥 ) )
13 12 notbid ⊢ ( 𝐾 ∈ Proset → ( ¬ 𝑥 ◡ ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑥 ) )
14 13 rabbidv ⊢ ( 𝐾 ∈ Proset → { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
15 14 mpteq2dv ⊢ ( 𝐾 ∈ Proset → ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) )
16 15 rneqd ⊢ ( 𝐾 ∈ Proset → ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) )
17 10 16 uneq12d ⊢ ( 𝐾 ∈ Proset → ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } ) ) = ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ) )
18 uncom ⊢ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ) = ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
19 17 18 eqtrdi ⊢ ( 𝐾 ∈ Proset → ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } ) ) = ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) )
20 19 uneq2d ⊢ ( 𝐾 ∈ Proset → ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } ) ) ) = ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) )
21 20 fveq2d ⊢ ( 𝐾 ∈ Proset → ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } ) ) ) ) = ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) )
22 21 fveq2d ⊢ ( 𝐾 ∈ Proset → ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } ) ) ) ) ) = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ) )
23 eqid ⊢ ( ODual ‘ 𝐾 ) = ( ODual ‘ 𝐾 )
24 23 oduprs ⊢ ( 𝐾 ∈ Proset → ( ODual ‘ 𝐾 ) ∈ Proset )
25 23 1 odubas ⊢ 𝐵 = ( Base ‘ ( ODual ‘ 𝐾 ) )
26 2 cnveqi ⊢ ◡ ≤ = ◡ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
27 cnvin ⊢ ◡ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) = ( ◡ ( le ‘ 𝐾 ) ∩ ◡ ( 𝐵 × 𝐵 ) )
28 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
29 23 28 oduleval ⊢ ◡ ( le ‘ 𝐾 ) = ( le ‘ ( ODual ‘ 𝐾 ) )
30 cnvxp ⊢ ◡ ( 𝐵 × 𝐵 ) = ( 𝐵 × 𝐵 )
31 29 30 ineq12i ⊢ ( ◡ ( le ‘ 𝐾 ) ∩ ◡ ( 𝐵 × 𝐵 ) ) = ( ( le ‘ ( ODual ‘ 𝐾 ) ) ∩ ( 𝐵 × 𝐵 ) )
32 26 27 31 3eqtri ⊢ ◡ ≤ = ( ( le ‘ ( ODual ‘ 𝐾 ) ) ∩ ( 𝐵 × 𝐵 ) )
33 eqid ⊢ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } )
34 eqid ⊢ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } )
35 25 32 33 34 ordtprsval ⊢ ( ( ODual ‘ 𝐾 ) ∈ Proset → ( ordTop ‘ ◡ ≤ ) = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } ) ) ) ) ) )
36 24 35 syl ⊢ ( 𝐾 ∈ Proset → ( ordTop ‘ ◡ ≤ ) = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ◡ ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ◡ ≤ 𝑦 } ) ) ) ) ) )
37 eqid ⊢ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
38 eqid ⊢ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
39 1 2 37 38 ordtprsval ⊢ ( 𝐾 ∈ Proset → ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ) )
40 22 36 39 3eqtr4d ⊢ ( 𝐾 ∈ Proset → ( ordTop ‘ ◡ ≤ ) = ( ordTop ‘ ≤ ) )