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 eqss ⊢ J ∩ Clsd ⁡ J = ∅ X ↔ J ∩ Clsd ⁡ J ⊆ ∅ X ∧ ∅ X ⊆ J ∩ Clsd ⁡ J
4 0opn ⊢ J ∈ Top → ∅ ∈ J
5 0cld ⊢ J ∈ Top → ∅ ∈ Clsd ⁡ J
6 4 5 elind ⊢ J ∈ Top → ∅ ∈ J ∩ Clsd ⁡ J
7 1 topopn ⊢ J ∈ Top → X ∈ J
8 1 topcld ⊢ J ∈ Top → X ∈ Clsd ⁡ J
9 7 8 elind ⊢ J ∈ Top → X ∈ J ∩ Clsd ⁡ J
10 6 9 prssd ⊢ J ∈ Top → ∅ X ⊆ J ∩ Clsd ⁡ J
11 10 biantrud ⊢ J ∈ Top → J ∩ Clsd ⁡ J ⊆ ∅ X ↔ J ∩ Clsd ⁡ J ⊆ ∅ X ∧ ∅ X ⊆ J ∩ Clsd ⁡ J
12 3 11 bitr4id ⊢ 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