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 ‘ 𝐽 ) ) ⊆ { ∅ , 𝑋 } ) )