Metamath Proof Explorer

Theorem isconn2

Description: The predicate J is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypothesis isconn.1 ⊢ 𝑋 = ∪ 𝐽
Assertion isconn2 ( 𝐽 ∈ Conn ↔ ( 𝐽 ∈ Top ∧ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 isconn.1 ⊢ 𝑋 = ∪ 𝐽
2 1 isconn ⊢ ( 𝐽 ∈ Conn ↔ ( 𝐽 ∈ Top ∧ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) = { ∅ , 𝑋 } ) )
3 eqss ⊢ ( ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) = { ∅ , 𝑋 } ↔ ( ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , 𝑋 } ∧ { ∅ , 𝑋 } ⊆ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ) )
4 0opn ⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
5 0cld ⊢ ( 𝐽 ∈ Top → ∅ ∈ ( Clsd ‘ 𝐽 ) )
6 4 5 elind ⊢ ( 𝐽 ∈ Top → ∅ ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) )
7 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
8 1 topcld ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
9 7 8 elind ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) )
10 6 9 prssd ⊢ ( 𝐽 ∈ Top → { ∅ , 𝑋 } ⊆ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) )
11 10 biantrud ⊢ ( 𝐽 ∈ Top → ( ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , 𝑋 } ↔ ( ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , 𝑋 } ∧ { ∅ , 𝑋 } ⊆ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ) ) )
12 3 11 bitr4id ⊢ ( 𝐽 ∈ Top → ( ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) = { ∅ , 𝑋 } ↔ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , 𝑋 } ) )
13 12 pm5.32i ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) = { ∅ , 𝑋 } ) ↔ ( 𝐽 ∈ Top ∧ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , 𝑋 } ) )
14 2 13 bitri ⊢ ( 𝐽 ∈ Conn ↔ ( 𝐽 ∈ Top ∧ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , 𝑋 } ) )