Metamath Proof Explorer

Theorem ordtval

Description: Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ordtval.1 ⊢ 𝑋 = dom 𝑅
ordtval.2 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
ordtval.3 ⊢ 𝐵 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
Assertion ordtval ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ordtval.1 ⊢ 𝑋 = dom 𝑅
2 ordtval.2 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
3 ordtval.3 ⊢ 𝐵 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
4 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
5 dmeq ⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
6 5 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → dom 𝑟 = 𝑋 )
7 6 sneqd ⊢ ( 𝑟 = 𝑅 → { dom 𝑟 } = { 𝑋 } )
8 rnun ⊢ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) = ( ran ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) )
9 breq ⊢ ( 𝑟 = 𝑅 → ( 𝑦 𝑟 𝑥 ↔ 𝑦 𝑅 𝑥 ) )
10 9 notbid ⊢ ( 𝑟 = 𝑅 → ( ¬ 𝑦 𝑟 𝑥 ↔ ¬ 𝑦 𝑅 𝑥 ) )
11 6 10 rabeqbidv ⊢ ( 𝑟 = 𝑅 → { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
12 6 11 mpteq12dv ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
13 12 rneqd ⊢ ( 𝑟 = 𝑅 → ran ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
14 13 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ran ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) = 𝐴 )
15 breq ⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
16 15 notbid ⊢ ( 𝑟 = 𝑅 → ( ¬ 𝑥 𝑟 𝑦 ↔ ¬ 𝑥 𝑅 𝑦 ) )
17 6 16 rabeqbidv ⊢ ( 𝑟 = 𝑅 → { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
18 6 17 mpteq12dv ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
19 18 rneqd ⊢ ( 𝑟 = 𝑅 → ran ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
20 19 3 eqtr4di ⊢ ( 𝑟 = 𝑅 → ran ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) = 𝐵 )
21 14 20 uneq12d ⊢ ( 𝑟 = 𝑅 → ( ran ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) = ( 𝐴 ∪ 𝐵 ) )
22 8 21 syl5eq ⊢ ( 𝑟 = 𝑅 → ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) = ( 𝐴 ∪ 𝐵 ) )
23 7 22 uneq12d ⊢ ( 𝑟 = 𝑅 → ( { dom 𝑟 } ∪ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) ) = ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) )
24 23 fveq2d ⊢ ( 𝑟 = 𝑅 → ( fi ‘ ( { dom 𝑟 } ∪ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) ) ) = ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) )
25 24 fveq2d ⊢ ( 𝑟 = 𝑅 → ( topGen ‘ ( fi ‘ ( { dom 𝑟 } ∪ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) ) ) ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) )
26 df-ordt ⊢ ordTop = ( 𝑟 ∈ V ↦ ( topGen ‘ ( fi ‘ ( { dom 𝑟 } ∪ ran ( ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦 𝑟 𝑥 } ) ∪ ( 𝑥 ∈ dom 𝑟 ↦ { 𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥 𝑟 𝑦 } ) ) ) ) ) )
27 fvex ⊢ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) ∈ V
28 25 26 27 fvmpt ⊢ ( 𝑅 ∈ V → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) )
29 4 28 syl ⊢ ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ) ) )