Metamath Proof Explorer


Theorem connsubclo

Description: If a clopen set meets a connected subspace, it must contain the entire subspace. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypotheses connsubclo.1 𝑋 = 𝐽
connsubclo.3 ( 𝜑𝐴𝑋 )
connsubclo.4 ( 𝜑 → ( 𝐽t 𝐴 ) ∈ Conn )
connsubclo.5 ( 𝜑𝐵𝐽 )
connsubclo.6 ( 𝜑 → ( 𝐵𝐴 ) ≠ ∅ )
connsubclo.7 ( 𝜑𝐵 ∈ ( Clsd ‘ 𝐽 ) )
Assertion connsubclo ( 𝜑𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 connsubclo.1 𝑋 = 𝐽
2 connsubclo.3 ( 𝜑𝐴𝑋 )
3 connsubclo.4 ( 𝜑 → ( 𝐽t 𝐴 ) ∈ Conn )
4 connsubclo.5 ( 𝜑𝐵𝐽 )
5 connsubclo.6 ( 𝜑 → ( 𝐵𝐴 ) ≠ ∅ )
6 connsubclo.7 ( 𝜑𝐵 ∈ ( Clsd ‘ 𝐽 ) )
7 eqid ( 𝐽t 𝐴 ) = ( 𝐽t 𝐴 )
8 cldrcl ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
9 6 8 syl ( 𝜑𝐽 ∈ Top )
10 1 topopn ( 𝐽 ∈ Top → 𝑋𝐽 )
11 9 10 syl ( 𝜑𝑋𝐽 )
12 11 2 ssexd ( 𝜑𝐴 ∈ V )
13 elrestr ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ 𝐵𝐽 ) → ( 𝐵𝐴 ) ∈ ( 𝐽t 𝐴 ) )
14 9 12 4 13 syl3anc ( 𝜑 → ( 𝐵𝐴 ) ∈ ( 𝐽t 𝐴 ) )
15 eqid ( 𝐵𝐴 ) = ( 𝐵𝐴 )
16 ineq1 ( 𝑥 = 𝐵 → ( 𝑥𝐴 ) = ( 𝐵𝐴 ) )
17 16 rspceeqv ( ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐵𝐴 ) = ( 𝐵𝐴 ) ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐵𝐴 ) = ( 𝑥𝐴 ) )
18 6 15 17 sylancl ( 𝜑 → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐵𝐴 ) = ( 𝑥𝐴 ) )
19 1 restcld ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → ( ( 𝐵𝐴 ) ∈ ( Clsd ‘ ( 𝐽t 𝐴 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐵𝐴 ) = ( 𝑥𝐴 ) ) )
20 9 2 19 syl2anc ( 𝜑 → ( ( 𝐵𝐴 ) ∈ ( Clsd ‘ ( 𝐽t 𝐴 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐵𝐴 ) = ( 𝑥𝐴 ) ) )
21 18 20 mpbird ( 𝜑 → ( 𝐵𝐴 ) ∈ ( Clsd ‘ ( 𝐽t 𝐴 ) ) )
22 7 3 14 5 21 connclo ( 𝜑 → ( 𝐵𝐴 ) = ( 𝐽t 𝐴 ) )
23 1 restuni ( ( 𝐽 ∈ Top ∧ 𝐴𝑋 ) → 𝐴 = ( 𝐽t 𝐴 ) )
24 9 2 23 syl2anc ( 𝜑𝐴 = ( 𝐽t 𝐴 ) )
25 22 24 eqtr4d ( 𝜑 → ( 𝐵𝐴 ) = 𝐴 )
26 sseqin2 ( 𝐴𝐵 ↔ ( 𝐵𝐴 ) = 𝐴 )
27 25 26 sylibr ( 𝜑𝐴𝐵 )