Metamath Proof Explorer

Theorem nconnsubb

Description: Disconnectedness for a subspace. (Contributed by FL, 29-May-2014) (Proof shortened by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypotheses nconnsubb.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
nconnsubb.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
nconnsubb.4 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
nconnsubb.5 ⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
nconnsubb.6 ⊢ ( 𝜑 → ( 𝑈 ∩ 𝐴 ) ≠ ∅ )
nconnsubb.7 ⊢ ( 𝜑 → ( 𝑉 ∩ 𝐴 ) ≠ ∅ )
nconnsubb.8 ⊢ ( 𝜑 → ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ )
nconnsubb.9 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) )
Assertion nconnsubb ( 𝜑 → ¬ ( 𝐽 ↾t 𝐴 ) ∈ Conn )

Proof

Step Hyp Ref Expression
1 nconnsubb.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 nconnsubb.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
3 nconnsubb.4 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
4 nconnsubb.5 ⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
5 nconnsubb.6 ⊢ ( 𝜑 → ( 𝑈 ∩ 𝐴 ) ≠ ∅ )
6 nconnsubb.7 ⊢ ( 𝜑 → ( 𝑉 ∩ 𝐴 ) ≠ ∅ )
7 nconnsubb.8 ⊢ ( 𝜑 → ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ )
8 nconnsubb.9 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) )
9 connsuba ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) )
10 1 2 9 syl2anc ⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) )
11 5 6 7 3jca ⊢ ( 𝜑 → ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) )
12 ineq1 ⊢ ( 𝑥 = 𝑈 → ( 𝑥 ∩ 𝐴 ) = ( 𝑈 ∩ 𝐴 ) )
13 12 neeq1d ⊢ ( 𝑥 = 𝑈 → ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ↔ ( 𝑈 ∩ 𝐴 ) ≠ ∅ ) )
14 ineq1 ⊢ ( 𝑥 = 𝑈 → ( 𝑥 ∩ 𝑦 ) = ( 𝑈 ∩ 𝑦 ) )
15 14 ineq1d ⊢ ( 𝑥 = 𝑈 → ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) )
16 15 eqeq1d ⊢ ( 𝑥 = 𝑈 → ( ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ↔ ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) )
17 13 16 3anbi13d ⊢ ( 𝑥 = 𝑈 → ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) ↔ ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) ) )
18 uneq1 ⊢ ( 𝑥 = 𝑈 → ( 𝑥 ∪ 𝑦 ) = ( 𝑈 ∪ 𝑦 ) )
19 18 ineq1d ⊢ ( 𝑥 = 𝑈 → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) = ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) )
20 19 neeq1d ⊢ ( 𝑥 = 𝑈 → ( ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ↔ ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) )
21 17 20 imbi12d ⊢ ( 𝑥 = 𝑈 → ( ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ↔ ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) )
22 ineq1 ⊢ ( 𝑦 = 𝑉 → ( 𝑦 ∩ 𝐴 ) = ( 𝑉 ∩ 𝐴 ) )
23 22 neeq1d ⊢ ( 𝑦 = 𝑉 → ( ( 𝑦 ∩ 𝐴 ) ≠ ∅ ↔ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ) )
24 ineq2 ⊢ ( 𝑦 = 𝑉 → ( 𝑈 ∩ 𝑦 ) = ( 𝑈 ∩ 𝑉 ) )
25 24 ineq1d ⊢ ( 𝑦 = 𝑉 → ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) )
26 25 eqeq1d ⊢ ( 𝑦 = 𝑉 → ( ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ↔ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) )
27 23 26 3anbi23d ⊢ ( 𝑦 = 𝑉 → ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) ↔ ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) ) )
28 sseqin2 ⊢ ( 𝐴 ⊆ ( 𝑈 ∪ 𝑦 ) ↔ ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) = 𝐴 )
29 28 necon3bbii ⊢ ( ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑦 ) ↔ ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 )
30 uneq2 ⊢ ( 𝑦 = 𝑉 → ( 𝑈 ∪ 𝑦 ) = ( 𝑈 ∪ 𝑉 ) )
31 30 sseq2d ⊢ ( 𝑦 = 𝑉 → ( 𝐴 ⊆ ( 𝑈 ∪ 𝑦 ) ↔ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) )
32 31 notbid ⊢ ( 𝑦 = 𝑉 → ( ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑦 ) ↔ ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) )
33 29 32 bitr3id ⊢ ( 𝑦 = 𝑉 → ( ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ↔ ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) )
34 27 33 imbi12d ⊢ ( 𝑦 = 𝑉 → ( ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ↔ ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) )
35 21 34 rspc2v ⊢ ( ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) → ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) )
36 3 4 35 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) → ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) )
37 11 36 mpid ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) )
38 10 37 sylbid ⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) )
39 8 38 mt2d ⊢ ( 𝜑 → ¬ ( 𝐽 ↾t 𝐴 ) ∈ Conn )