This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem toplatjoin

Description: Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024)

Ref Expression
Hypotheses toplatmeet.i ⊢ 𝐼 = ( toInc ‘ 𝐽 )
toplatmeet.j ⊢ ( 𝜑 → 𝐽 ∈ Top )
toplatmeet.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
toplatmeet.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
toplatjoin.j ⊢ ∨ = ( join ‘ 𝐼 )
Assertion toplatjoin ( 𝜑 → ( 𝐴 ∨ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 toplatmeet.i ⊢ 𝐼 = ( toInc ‘ 𝐽 )
2 toplatmeet.j ⊢ ( 𝜑 → 𝐽 ∈ Top )
3 toplatmeet.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
4 toplatmeet.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
5 toplatjoin.j ⊢ ∨ = ( join ‘ 𝐼 )
6 eqid ⊢ ( lub ‘ 𝐼 ) = ( lub ‘ 𝐼 )
7 1 ipopos ⊢ 𝐼 ∈ Poset
8 7 a1i ⊢ ( 𝜑 → 𝐼 ∈ Poset )
9 6 5 8 3 4 joinval ⊢ ( 𝜑 → ( 𝐴 ∨ 𝐵 ) = ( ( lub ‘ 𝐼 ) ‘ { 𝐴 , 𝐵 } ) )
10 3 4 prssd ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ 𝐽 )
11 6 a1i ⊢ ( 𝜑 → ( lub ‘ 𝐼 ) = ( lub ‘ 𝐼 ) )
12 uniprg ⊢ ( ( 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
13 3 4 12 syl2anc ⊢ ( 𝜑 → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
14 unopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝐽 )
15 2 3 4 14 syl3anc ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ 𝐽 )
16 13 15 eqeltrd ⊢ ( 𝜑 → ∪ { 𝐴 , 𝐵 } ∈ 𝐽 )
17 intmin ⊢ ( ∪ { 𝐴 , 𝐵 } ∈ 𝐽 → ∩ { 𝑥 ∈ 𝐽 ∣ ∪ { 𝐴 , 𝐵 } ⊆ 𝑥 } = ∪ { 𝐴 , 𝐵 } )
18 16 17 syl ⊢ ( 𝜑 → ∩ { 𝑥 ∈ 𝐽 ∣ ∪ { 𝐴 , 𝐵 } ⊆ 𝑥 } = ∪ { 𝐴 , 𝐵 } )
19 18 13 eqtr2d ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = ∩ { 𝑥 ∈ 𝐽 ∣ ∪ { 𝐴 , 𝐵 } ⊆ 𝑥 } )
20 1 2 10 11 19 15 ipolub ⊢ ( 𝜑 → ( ( lub ‘ 𝐼 ) ‘ { 𝐴 , 𝐵 } ) = ( 𝐴 ∪ 𝐵 ) )
21 9 20 eqtrd ⊢ ( 𝜑 → ( 𝐴 ∨ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )