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

Metamath Proof Explorer

Theorem isconn

Description: The predicate J is a connected topology . (Contributed by FL, 17-Nov-2008)

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

Proof

Step Hyp Ref Expression
1 isconn.1 ⊢ 𝑋 = ∪ 𝐽
2 id ⊢ ( 𝑗 = 𝐽 → 𝑗 = 𝐽 )
3 fveq2 ⊢ ( 𝑗 = 𝐽 → ( Clsd ‘ 𝑗 ) = ( Clsd ‘ 𝐽 ) )
4 2 3 ineq12d ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ∩ ( Clsd ‘ 𝑗 ) ) = ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) )
5 unieq ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
6 5 1 eqtr4di ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = 𝑋 )
7 6 preq2d ⊢ ( 𝑗 = 𝐽 → { ∅ , ∪ 𝑗 } = { ∅ , 𝑋 } )
8 4 7 eqeq12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 ∩ ( Clsd ‘ 𝑗 ) ) = { ∅ , ∪ 𝑗 } ↔ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) = { ∅ , 𝑋 } ) )
9 df-conn ⊢ Conn = { 𝑗 ∈ Top ∣ ( 𝑗 ∩ ( Clsd ‘ 𝑗 ) ) = { ∅ , ∪ 𝑗 } }
10 8 9 elrab2 ⊢ ( 𝐽 ∈ Conn ↔ ( 𝐽 ∈ Top ∧ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) = { ∅ , 𝑋 } ) )