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

Metamath Proof Explorer

Theorem connsub

Description: Two equivalent ways of saying that a subspace topology is connected. (Contributed by Jeff Hankins, 9-Jul-2009) (Proof shortened by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion connsub ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) → ¬ 𝑆 ⊆ ( 𝑥 ∪ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 connsuba ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝑆 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑆 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝑆 ) ≠ 𝑆 ) ) )
2 inss1 ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑥
3 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝑋 )
4 3 ad2ant2r ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑥 ⊆ 𝑋 )
5 2 4 sstrid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 )
6 reldisj ⊢ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 → ( ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑆 ) = ∅ ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
7 5 6 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑆 ) = ∅ ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
8 7 3anbi3d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝑆 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑆 ) = ∅ ) ↔ ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) ) )
9 sseqin2 ⊢ ( 𝑆 ⊆ ( 𝑥 ∪ 𝑦 ) ↔ ( ( 𝑥 ∪ 𝑦 ) ∩ 𝑆 ) = 𝑆 )
10 9 a1i ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑆 ⊆ ( 𝑥 ∪ 𝑦 ) ↔ ( ( 𝑥 ∪ 𝑦 ) ∩ 𝑆 ) = 𝑆 ) )
11 10 bicomd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( ( 𝑥 ∪ 𝑦 ) ∩ 𝑆 ) = 𝑆 ↔ 𝑆 ⊆ ( 𝑥 ∪ 𝑦 ) ) )
12 11 necon3abid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( ( 𝑥 ∪ 𝑦 ) ∩ 𝑆 ) ≠ 𝑆 ↔ ¬ 𝑆 ⊆ ( 𝑥 ∪ 𝑦 ) ) )
13 8 12 imbi12d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝑆 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑆 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝑆 ) ≠ 𝑆 ) ↔ ( ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) → ¬ 𝑆 ⊆ ( 𝑥 ∪ 𝑦 ) ) ) )
14 13 2ralbidva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝑆 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑆 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝑆 ) ≠ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) → ¬ 𝑆 ⊆ ( 𝑥 ∪ 𝑦 ) ) ) )
15 1 14 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) → ¬ 𝑆 ⊆ ( 𝑥 ∪ 𝑦 ) ) ) )