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 )