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