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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
ordtNEW.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
ordtposval.e ⊢ 𝐸 = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
ordtposval.f ⊢ 𝐹 = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
Assertion ordtprsval ( 𝐾 ∈ Proset → ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( 𝐸 ∪ 𝐹 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ordtNEW.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ordtNEW.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3 ordtposval.e ⊢ 𝐸 = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
4 ordtposval.f ⊢ 𝐹 = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
5 fvex ⊢ ( le ‘ 𝐾 ) ∈ V
6 5 inex1 ⊢ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ∈ V
7 2 6 eqeltri ⊢ ≤ ∈ V
8 eqid ⊢ dom ≤ = dom ≤
9 eqid ⊢ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) = ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } )
10 eqid ⊢ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) = ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } )
11 8 9 10 ordtval ⊢ ( ≤ ∈ V → ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( { dom ≤ } ∪ ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ) )
12 7 11 ax-mp ⊢ ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( { dom ≤ } ∪ ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) )
13 1 2 prsdm ⊢ ( 𝐾 ∈ Proset → dom ≤ = 𝐵 )
14 13 sneqd ⊢ ( 𝐾 ∈ Proset → { dom ≤ } = { 𝐵 } )
15 13 rabeqdv ⊢ ( 𝐾 ∈ Proset → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
16 13 15 mpteq12dv ⊢ ( 𝐾 ∈ Proset → ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) )
17 16 rneqd ⊢ ( 𝐾 ∈ Proset → ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) )
18 17 3 eqtr4di ⊢ ( 𝐾 ∈ Proset → ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) = 𝐸 )
19 13 rabeqdv ⊢ ( 𝐾 ∈ Proset → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
20 13 19 mpteq12dv ⊢ ( 𝐾 ∈ Proset → ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
21 20 rneqd ⊢ ( 𝐾 ∈ Proset → ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
22 21 4 eqtr4di ⊢ ( 𝐾 ∈ Proset → ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) = 𝐹 )
23 18 22 uneq12d ⊢ ( 𝐾 ∈ Proset → ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) = ( 𝐸 ∪ 𝐹 ) )
24 14 23 uneq12d ⊢ ( 𝐾 ∈ Proset → ( { dom ≤ } ∪ ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) = ( { 𝐵 } ∪ ( 𝐸 ∪ 𝐹 ) ) )
25 24 fveq2d ⊢ ( 𝐾 ∈ Proset → ( fi ‘ ( { dom ≤ } ∪ ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) = ( fi ‘ ( { 𝐵 } ∪ ( 𝐸 ∪ 𝐹 ) ) ) )
26 25 fveq2d ⊢ ( 𝐾 ∈ Proset → ( topGen ‘ ( fi ‘ ( { dom ≤ } ∪ ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) ) ) = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( 𝐸 ∪ 𝐹 ) ) ) ) )
27 12 26 eqtrid ⊢ ( 𝐾 ∈ Proset → ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( 𝐸 ∪ 𝐹 ) ) ) ) )