Metamath Proof Explorer

Theorem dfconn2

Description: An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009) (Proof shortened by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion dfconn2 ⊢J∈TopOn⁡X→J∈Conn↔∀x∈J∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠X

Proof

Step Hyp Ref Expression
1 eqid ⊢⋃J=⋃J
2 simpll ⊢J∈Conn∧x∈J∧y∈J∧x≠∅∧y≠∅∧x∩y=∅→J∈Conn
3 simplrl ⊢J∈Conn∧x∈J∧y∈J∧x≠∅∧y≠∅∧x∩y=∅→x∈J
4 simpr1 ⊢J∈Conn∧x∈J∧y∈J∧x≠∅∧y≠∅∧x∩y=∅→x≠∅
5 simplrr ⊢J∈Conn∧x∈J∧y∈J∧x≠∅∧y≠∅∧x∩y=∅→y∈J
6 simpr2 ⊢J∈Conn∧x∈J∧y∈J∧x≠∅∧y≠∅∧x∩y=∅→y≠∅
7 simpr3 ⊢J∈Conn∧x∈J∧y∈J∧x≠∅∧y≠∅∧x∩y=∅→x∩y=∅
8 1 2 3 4 5 6 7 conndisj ⊢J∈Conn∧x∈J∧y∈J∧x≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J
9 8 ex ⊢J∈Conn∧x∈J∧y∈J→x≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J
10 9 ralrimivva ⊢J∈Conn→∀x∈J∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J
11 topontop ⊢J∈TopOn⁡X→J∈Top
12 1 cldopn ⊢x∈Clsd⁡J→⋃J∖x∈J
13 12 adantl ⊢J∈Top∧x∈Clsd⁡J→⋃J∖x∈J
14 df-3an ⊢x≠∅∧y≠∅∧x∩y=∅↔x≠∅∧y≠∅∧x∩y=∅
15 ineq2 ⊢y=⋃J∖x→x∩y=x∩⋃J∖x
16 disjdif ⊢x∩⋃J∖x=∅
17 15 16 eqtrdi ⊢y=⋃J∖x→x∩y=∅
18 17 biantrud ⊢y=⋃J∖x→x≠∅∧y≠∅↔x≠∅∧y≠∅∧x∩y=∅
19 neeq1 ⊢y=⋃J∖x→y≠∅↔⋃J∖x≠∅
20 19 anbi2d ⊢y=⋃J∖x→x≠∅∧y≠∅↔x≠∅∧⋃J∖x≠∅
21 18 20 bitr3d ⊢y=⋃J∖x→x≠∅∧y≠∅∧x∩y=∅↔x≠∅∧⋃J∖x≠∅
22 14 21 bitrid ⊢y=⋃J∖x→x≠∅∧y≠∅∧x∩y=∅↔x≠∅∧⋃J∖x≠∅
23 uneq2 ⊢y=⋃J∖x→x∪y=x∪⋃J∖x
24 undif2 ⊢x∪⋃J∖x=x∪⋃J
25 23 24 eqtrdi ⊢y=⋃J∖x→x∪y=x∪⋃J
26 25 neeq1d ⊢y=⋃J∖x→x∪y≠⋃J↔x∪⋃J≠⋃J
27 22 26 imbi12d ⊢y=⋃J∖x→x≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J↔x≠∅∧⋃J∖x≠∅→x∪⋃J≠⋃J
28 27 rspcv ⊢⋃J∖x∈J→∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→x≠∅∧⋃J∖x≠∅→x∪⋃J≠⋃J
29 13 28 syl ⊢J∈Top∧x∈Clsd⁡J→∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→x≠∅∧⋃J∖x≠∅→x∪⋃J≠⋃J
30 1 cldss ⊢x∈Clsd⁡J→x⊆⋃J
31 30 adantl ⊢J∈Top∧x∈Clsd⁡J→x⊆⋃J
32 ssequn1 ⊢x⊆⋃J↔x∪⋃J=⋃J
33 31 32 sylib ⊢J∈Top∧x∈Clsd⁡J→x∪⋃J=⋃J
34 ssdif0 ⊢⋃J⊆x↔⋃J∖x=∅
35 idd ⊢J∈Top∧x∈Clsd⁡J→⋃J⊆x→⋃J⊆x
36 35 31 jctild ⊢J∈Top∧x∈Clsd⁡J→⋃J⊆x→x⊆⋃J∧⋃J⊆x
37 eqss ⊢x=⋃J↔x⊆⋃J∧⋃J⊆x
38 36 37 syl6ibr ⊢J∈Top∧x∈Clsd⁡J→⋃J⊆x→x=⋃J
39 34 38 biimtrrid ⊢J∈Top∧x∈Clsd⁡J→⋃J∖x=∅→x=⋃J
40 33 39 embantd ⊢J∈Top∧x∈Clsd⁡J→x∪⋃J=⋃J→⋃J∖x=∅→x=⋃J
41 40 orim2d ⊢J∈Top∧x∈Clsd⁡J→x=∅∨x∪⋃J=⋃J→⋃J∖x=∅→x=∅∨x=⋃J
42 impexp ⊢x≠∅∧⋃J∖x≠∅→x∪⋃J≠⋃J↔x≠∅→⋃J∖x≠∅→x∪⋃J≠⋃J
43 df-ne ⊢x≠∅↔¬x=∅
44 id ⊢⋃J∖x≠∅→x∪⋃J≠⋃J→⋃J∖x≠∅→x∪⋃J≠⋃J
45 44 necon4d ⊢⋃J∖x≠∅→x∪⋃J≠⋃J→x∪⋃J=⋃J→⋃J∖x=∅
46 id ⊢x∪⋃J=⋃J→⋃J∖x=∅→x∪⋃J=⋃J→⋃J∖x=∅
47 46 necon3d ⊢x∪⋃J=⋃J→⋃J∖x=∅→⋃J∖x≠∅→x∪⋃J≠⋃J
48 45 47 impbii ⊢⋃J∖x≠∅→x∪⋃J≠⋃J↔x∪⋃J=⋃J→⋃J∖x=∅
49 43 48 imbi12i ⊢x≠∅→⋃J∖x≠∅→x∪⋃J≠⋃J↔¬x=∅→x∪⋃J=⋃J→⋃J∖x=∅
50 pm4.64 ⊢¬x=∅→x∪⋃J=⋃J→⋃J∖x=∅↔x=∅∨x∪⋃J=⋃J→⋃J∖x=∅
51 49 50 bitri ⊢x≠∅→⋃J∖x≠∅→x∪⋃J≠⋃J↔x=∅∨x∪⋃J=⋃J→⋃J∖x=∅
52 42 51 bitri ⊢x≠∅∧⋃J∖x≠∅→x∪⋃J≠⋃J↔x=∅∨x∪⋃J=⋃J→⋃J∖x=∅
53 vex ⊢x∈V
54 53 elpr ⊢x∈∅⋃J↔x=∅∨x=⋃J
55 41 52 54 3imtr4g ⊢J∈Top∧x∈Clsd⁡J→x≠∅∧⋃J∖x≠∅→x∪⋃J≠⋃J→x∈∅⋃J
56 29 55 syld ⊢J∈Top∧x∈Clsd⁡J→∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→x∈∅⋃J
57 56 ex ⊢J∈Top→x∈Clsd⁡J→∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→x∈∅⋃J
58 57 com23 ⊢J∈Top→∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→x∈Clsd⁡J→x∈∅⋃J
59 58 imim2d ⊢J∈Top→x∈J→∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→x∈J→x∈Clsd⁡J→x∈∅⋃J
60 elin ⊢x∈J∩Clsd⁡J↔x∈J∧x∈Clsd⁡J
61 60 imbi1i ⊢x∈J∩Clsd⁡J→x∈∅⋃J↔x∈J∧x∈Clsd⁡J→x∈∅⋃J
62 impexp ⊢x∈J∧x∈Clsd⁡J→x∈∅⋃J↔x∈J→x∈Clsd⁡J→x∈∅⋃J
63 61 62 bitri ⊢x∈J∩Clsd⁡J→x∈∅⋃J↔x∈J→x∈Clsd⁡J→x∈∅⋃J
64 59 63 syl6ibr ⊢J∈Top→x∈J→∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→x∈J∩Clsd⁡J→x∈∅⋃J
65 64 alimdv ⊢J∈Top→∀xx∈J→∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→∀xx∈J∩Clsd⁡J→x∈∅⋃J
66 df-ral ⊢∀x∈J∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J↔∀xx∈J→∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J
67 dfss2 ⊢J∩Clsd⁡J⊆∅⋃J↔∀xx∈J∩Clsd⁡J→x∈∅⋃J
68 65 66 67 3imtr4g ⊢J∈Top→∀x∈J∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→J∩Clsd⁡J⊆∅⋃J
69 1 isconn2 ⊢J∈Conn↔J∈Top∧J∩Clsd⁡J⊆∅⋃J
70 69 baib ⊢J∈Top→J∈Conn↔J∩Clsd⁡J⊆∅⋃J
71 68 70 sylibrd ⊢J∈Top→∀x∈J∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→J∈Conn
72 11 71 syl ⊢J∈TopOn⁡X→∀x∈J∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J→J∈Conn
73 10 72 impbid2 ⊢J∈TopOn⁡X→J∈Conn↔∀x∈J∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J
74 toponuni ⊢J∈TopOn⁡X→X=⋃J
75 74 neeq2d ⊢J∈TopOn⁡X→x∪y≠X↔x∪y≠⋃J
76 75 imbi2d ⊢J∈TopOn⁡X→x≠∅∧y≠∅∧x∩y=∅→x∪y≠X↔x≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J
77 76 2ralbidv ⊢J∈TopOn⁡X→∀x∈J∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠X↔∀x∈J∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠⋃J
78 73 77 bitr4d ⊢J∈TopOn⁡X→J∈Conn↔∀x∈J∀y∈Jx≠∅∧y≠∅∧x∩y=∅→x∪y≠X