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 ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝑆 ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) → ¬ 𝑆 ⊆ ( 𝑥 ∪ 𝑦 ) ) ) )