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 ⊢ X = ⋃ J
Assertion isconn2 ⊢ J ∈ Conn ↔ J ∈ Top ∧ J ∩ Clsd ⁡ J ⊆ ∅ X

Proof

Step Hyp Ref Expression
1 isconn.1 ⊢ X = ⋃ J
2 1 isconn ⊢ J ∈ Conn ↔ J ∈ Top ∧ J ∩ Clsd ⁡ J = ∅ X
3 0opn ⊢ J ∈ Top → ∅ ∈ J
4 0cld ⊢ J ∈ Top → ∅ ∈ Clsd ⁡ J
5 3 4 elind ⊢ J ∈ Top → ∅ ∈ J ∩ Clsd ⁡ J
6 1 topopn ⊢ J ∈ Top → X ∈ J
7 1 topcld ⊢ J ∈ Top → X ∈ Clsd ⁡ J
8 6 7 elind ⊢ J ∈ Top → X ∈ J ∩ Clsd ⁡ J
9 5 8 prssd ⊢ J ∈ Top → ∅ X ⊆ J ∩ Clsd ⁡ J
10 9 biantrud ⊢ J ∈ Top → J ∩ Clsd ⁡ J ⊆ ∅ X ↔ J ∩ Clsd ⁡ J ⊆ ∅ X ∧ ∅ X ⊆ J ∩ Clsd ⁡ J
11 eqss ⊢ J ∩ Clsd ⁡ J = ∅ X ↔ J ∩ Clsd ⁡ J ⊆ ∅ X ∧ ∅ X ⊆ J ∩ Clsd ⁡ J
12 10 11 syl6rbbr ⊢ J ∈ Top → J ∩ Clsd ⁡ J = ∅ X ↔ J ∩ Clsd ⁡ J ⊆ ∅ X
13 12 pm5.32i ⊢ J ∈ Top ∧ J ∩ Clsd ⁡ J = ∅ X ↔ J ∈ Top ∧ J ∩ Clsd ⁡ J ⊆ ∅ X
14 2 13 bitri ⊢ J ∈ Conn ↔ J ∈ Top ∧ J ∩ Clsd ⁡ J ⊆ ∅ X