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 e. ( TopOn ` X ) -> ( J e. Conn <-> A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= X ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 simpll 
 |-  ( ( ( J e. Conn /\ ( x e. J /\ y e. J ) ) /\ ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) ) -> J e. Conn )
3 simplrl 
 |-  ( ( ( J e. Conn /\ ( x e. J /\ y e. J ) ) /\ ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) ) -> x e. J )
4 simpr1 
 |-  ( ( ( J e. Conn /\ ( x e. J /\ y e. J ) ) /\ ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) ) -> x =/= (/) )
5 simplrr 
 |-  ( ( ( J e. Conn /\ ( x e. J /\ y e. J ) ) /\ ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) ) -> y e. J )
6 simpr2 
 |-  ( ( ( J e. Conn /\ ( x e. J /\ y e. J ) ) /\ ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) ) -> y =/= (/) )
7 simpr3 
 |-  ( ( ( J e. Conn /\ ( x e. J /\ y e. J ) ) /\ ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) ) -> ( x i^i y ) = (/) )
8 1 2 3 4 5 6 7 conndisj 
 |-  ( ( ( J e. Conn /\ ( x e. J /\ y e. J ) ) /\ ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) ) -> ( x u. y ) =/= U. J )
9 8 ex 
 |-  ( ( J e. Conn /\ ( x e. J /\ y e. J ) ) -> ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) )
10 9 ralrimivva 
 |-  ( J e. Conn -> A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) )
11 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
12 1 cldopn 
 |-  ( x e. ( Clsd ` J ) -> ( U. J \ x ) e. J )
13 12 adantl 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( U. J \ x ) e. J )
14 df-3an 
 |-  ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) <-> ( ( x =/= (/) /\ y =/= (/) ) /\ ( x i^i y ) = (/) ) )
15 ineq2 
 |-  ( y = ( U. J \ x ) -> ( x i^i y ) = ( x i^i ( U. J \ x ) ) )
16 disjdif 
 |-  ( x i^i ( U. J \ x ) ) = (/)
17 15 16 eqtrdi 
 |-  ( y = ( U. J \ x ) -> ( x i^i y ) = (/) )
18 17 biantrud 
 |-  ( y = ( U. J \ x ) -> ( ( x =/= (/) /\ y =/= (/) ) <-> ( ( x =/= (/) /\ y =/= (/) ) /\ ( x i^i y ) = (/) ) ) )
19 neeq1 
 |-  ( y = ( U. J \ x ) -> ( y =/= (/) <-> ( U. J \ x ) =/= (/) ) )
20 19 anbi2d 
 |-  ( y = ( U. J \ x ) -> ( ( x =/= (/) /\ y =/= (/) ) <-> ( x =/= (/) /\ ( U. J \ x ) =/= (/) ) ) )
21 18 20 bitr3d 
 |-  ( y = ( U. J \ x ) -> ( ( ( x =/= (/) /\ y =/= (/) ) /\ ( x i^i y ) = (/) ) <-> ( x =/= (/) /\ ( U. J \ x ) =/= (/) ) ) )
22 14 21 bitrid 
 |-  ( y = ( U. J \ x ) -> ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) <-> ( x =/= (/) /\ ( U. J \ x ) =/= (/) ) ) )
23 uneq2 
 |-  ( y = ( U. J \ x ) -> ( x u. y ) = ( x u. ( U. J \ x ) ) )
24 undif2 
 |-  ( x u. ( U. J \ x ) ) = ( x u. U. J )
25 23 24 eqtrdi 
 |-  ( y = ( U. J \ x ) -> ( x u. y ) = ( x u. U. J ) )
26 25 neeq1d 
 |-  ( y = ( U. J \ x ) -> ( ( x u. y ) =/= U. J <-> ( x u. U. J ) =/= U. J ) )
27 22 26 imbi12d 
 |-  ( y = ( U. J \ x ) -> ( ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) <-> ( ( x =/= (/) /\ ( U. J \ x ) =/= (/) ) -> ( x u. U. J ) =/= U. J ) ) )
28 27 rspcv 
 |-  ( ( U. J \ x ) e. J -> ( A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) -> ( ( x =/= (/) /\ ( U. J \ x ) =/= (/) ) -> ( x u. U. J ) =/= U. J ) ) )
29 13 28 syl 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) -> ( ( x =/= (/) /\ ( U. J \ x ) =/= (/) ) -> ( x u. U. J ) =/= U. J ) ) )
30 1 cldss 
 |-  ( x e. ( Clsd ` J ) -> x C_ U. J )
31 30 adantl 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> x C_ U. J )
32 ssequn1 
 |-  ( x C_ U. J <-> ( x u. U. J ) = U. J )
33 31 32 sylib 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( x u. U. J ) = U. J )
34 ssdif0 
 |-  ( U. J C_ x <-> ( U. J \ x ) = (/) )
35 idd 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( U. J C_ x -> U. J C_ x ) )
36 35 31 jctild 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( U. J C_ x -> ( x C_ U. J /\ U. J C_ x ) ) )
37 eqss 
 |-  ( x = U. J <-> ( x C_ U. J /\ U. J C_ x ) )
38 36 37 imbitrrdi 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( U. J C_ x -> x = U. J ) )
39 34 38 biimtrrid 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( ( U. J \ x ) = (/) -> x = U. J ) )
40 33 39 embantd 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) -> x = U. J ) )
41 40 orim2d 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( ( x = (/) \/ ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) ) -> ( x = (/) \/ x = U. J ) ) )
42 impexp 
 |-  ( ( ( x =/= (/) /\ ( U. J \ x ) =/= (/) ) -> ( x u. U. J ) =/= U. J ) <-> ( x =/= (/) -> ( ( U. J \ x ) =/= (/) -> ( x u. U. J ) =/= U. J ) ) )
43 df-ne 
 |-  ( x =/= (/) <-> -. x = (/) )
44 id 
 |-  ( ( ( U. J \ x ) =/= (/) -> ( x u. U. J ) =/= U. J ) -> ( ( U. J \ x ) =/= (/) -> ( x u. U. J ) =/= U. J ) )
45 44 necon4d 
 |-  ( ( ( U. J \ x ) =/= (/) -> ( x u. U. J ) =/= U. J ) -> ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) )
46 id 
 |-  ( ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) -> ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) )
47 46 necon3d 
 |-  ( ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) -> ( ( U. J \ x ) =/= (/) -> ( x u. U. J ) =/= U. J ) )
48 45 47 impbii 
 |-  ( ( ( U. J \ x ) =/= (/) -> ( x u. U. J ) =/= U. J ) <-> ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) )
49 43 48 imbi12i 
 |-  ( ( x =/= (/) -> ( ( U. J \ x ) =/= (/) -> ( x u. U. J ) =/= U. J ) ) <-> ( -. x = (/) -> ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) ) )
50 pm4.64 
 |-  ( ( -. x = (/) -> ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) ) <-> ( x = (/) \/ ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) ) )
51 49 50 bitri 
 |-  ( ( x =/= (/) -> ( ( U. J \ x ) =/= (/) -> ( x u. U. J ) =/= U. J ) ) <-> ( x = (/) \/ ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) ) )
52 42 51 bitri 
 |-  ( ( ( x =/= (/) /\ ( U. J \ x ) =/= (/) ) -> ( x u. U. J ) =/= U. J ) <-> ( x = (/) \/ ( ( x u. U. J ) = U. J -> ( U. J \ x ) = (/) ) ) )
53 vex 
 |-  x e. _V
54 53 elpr 
 |-  ( x e. { (/) , U. J } <-> ( x = (/) \/ x = U. J ) )
55 41 52 54 3imtr4g 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( ( ( x =/= (/) /\ ( U. J \ x ) =/= (/) ) -> ( x u. U. J ) =/= U. J ) -> x e. { (/) , U. J } ) )
56 29 55 syld 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) -> x e. { (/) , U. J } ) )
57 56 ex 
 |-  ( J e. Top -> ( x e. ( Clsd ` J ) -> ( A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) -> x e. { (/) , U. J } ) ) )
58 57 com23 
 |-  ( J e. Top -> ( A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) -> ( x e. ( Clsd ` J ) -> x e. { (/) , U. J } ) ) )
59 58 imim2d 
 |-  ( J e. Top -> ( ( x e. J -> A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) ) -> ( x e. J -> ( x e. ( Clsd ` J ) -> x e. { (/) , U. J } ) ) ) )
60 elin 
 |-  ( x e. ( J i^i ( Clsd ` J ) ) <-> ( x e. J /\ x e. ( Clsd ` J ) ) )
61 60 imbi1i 
 |-  ( ( x e. ( J i^i ( Clsd ` J ) ) -> x e. { (/) , U. J } ) <-> ( ( x e. J /\ x e. ( Clsd ` J ) ) -> x e. { (/) , U. J } ) )
62 impexp 
 |-  ( ( ( x e. J /\ x e. ( Clsd ` J ) ) -> x e. { (/) , U. J } ) <-> ( x e. J -> ( x e. ( Clsd ` J ) -> x e. { (/) , U. J } ) ) )
63 61 62 bitri 
 |-  ( ( x e. ( J i^i ( Clsd ` J ) ) -> x e. { (/) , U. J } ) <-> ( x e. J -> ( x e. ( Clsd ` J ) -> x e. { (/) , U. J } ) ) )
64 59 63 imbitrrdi 
 |-  ( J e. Top -> ( ( x e. J -> A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) ) -> ( x e. ( J i^i ( Clsd ` J ) ) -> x e. { (/) , U. J } ) ) )
65 64 alimdv 
 |-  ( J e. Top -> ( A. x ( x e. J -> A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) ) -> A. x ( x e. ( J i^i ( Clsd ` J ) ) -> x e. { (/) , U. J } ) ) )
66 df-ral 
 |-  ( A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) <-> A. x ( x e. J -> A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) ) )
67 df-ss 
 |-  ( ( J i^i ( Clsd ` J ) ) C_ { (/) , U. J } <-> A. x ( x e. ( J i^i ( Clsd ` J ) ) -> x e. { (/) , U. J } ) )
68 65 66 67 3imtr4g 
 |-  ( J e. Top -> ( A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) -> ( J i^i ( Clsd ` J ) ) C_ { (/) , U. J } ) )
69 1 isconn2 
 |-  ( J e. Conn <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) C_ { (/) , U. J } ) )
70 69 baib 
 |-  ( J e. Top -> ( J e. Conn <-> ( J i^i ( Clsd ` J ) ) C_ { (/) , U. J } ) )
71 68 70 sylibrd 
 |-  ( J e. Top -> ( A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) -> J e. Conn ) )
72 11 71 syl 
 |-  ( J e. ( TopOn ` X ) -> ( A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) -> J e. Conn ) )
73 10 72 impbid2 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Conn <-> A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) ) )
74 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
75 74 neeq2d 
 |-  ( J e. ( TopOn ` X ) -> ( ( x u. y ) =/= X <-> ( x u. y ) =/= U. J ) )
76 75 imbi2d 
 |-  ( J e. ( TopOn ` X ) -> ( ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= X ) <-> ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) ) )
77 76 2ralbidv 
 |-  ( J e. ( TopOn ` X ) -> ( A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= X ) <-> A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= U. J ) ) )
78 73 77 bitr4d 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Conn <-> A. x e. J A. y e. J ( ( x =/= (/) /\ y =/= (/) /\ ( x i^i y ) = (/) ) -> ( x u. y ) =/= X ) ) )