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 φJTopOnX
nconnsubb.3 φAX
nconnsubb.4 φUJ
nconnsubb.5 φVJ
nconnsubb.6 φUA
nconnsubb.7 φVA
nconnsubb.8 φUVA=
nconnsubb.9 φAUV
Assertion nconnsubb φ¬J𝑡AConn

Proof

Step Hyp Ref Expression
1 nconnsubb.2 φJTopOnX
2 nconnsubb.3 φAX
3 nconnsubb.4 φUJ
4 nconnsubb.5 φVJ
5 nconnsubb.6 φUA
6 nconnsubb.7 φVA
7 nconnsubb.8 φUVA=
8 nconnsubb.9 φAUV
9 connsuba JTopOnXAXJ𝑡AConnxJyJxAyAxyA=xyAA
10 1 2 9 syl2anc φJ𝑡AConnxJyJxAyAxyA=xyAA
11 5 6 7 3jca φUAVAUVA=
12 ineq1 x=UxA=UA
13 12 neeq1d x=UxAUA
14 ineq1 x=Uxy=Uy
15 14 ineq1d x=UxyA=UyA
16 15 eqeq1d x=UxyA=UyA=
17 13 16 3anbi13d x=UxAyAxyA=UAyAUyA=
18 uneq1 x=Uxy=Uy
19 18 ineq1d x=UxyA=UyA
20 19 neeq1d x=UxyAAUyAA
21 17 20 imbi12d x=UxAyAxyA=xyAAUAyAUyA=UyAA
22 ineq1 y=VyA=VA
23 22 neeq1d y=VyAVA
24 ineq2 y=VUy=UV
25 24 ineq1d y=VUyA=UVA
26 25 eqeq1d y=VUyA=UVA=
27 23 26 3anbi23d y=VUAyAUyA=UAVAUVA=
28 sseqin2 AUyUyA=A
29 28 necon3bbii ¬AUyUyAA
30 uneq2 y=VUy=UV
31 30 sseq2d y=VAUyAUV
32 31 notbid y=V¬AUy¬AUV
33 29 32 bitr3id y=VUyAA¬AUV
34 27 33 imbi12d y=VUAyAUyA=UyAAUAVAUVA=¬AUV
35 21 34 rspc2v UJVJxJyJxAyAxyA=xyAAUAVAUVA=¬AUV
36 3 4 35 syl2anc φxJyJxAyAxyA=xyAAUAVAUVA=¬AUV
37 11 36 mpid φxJyJxAyAxyA=xyAA¬AUV
38 10 37 sylbid φJ𝑡AConn¬AUV
39 8 38 mt2d φ¬J𝑡AConn