Metamath Proof Explorer

Theorem iunconn

Description: The indexed union of connected overlapping subspaces sharing a common point is connected. (Contributed by Mario Carneiro, 11-Jun-2014)

Ref Expression
Hypotheses iunconn.2 
|- ( ph -> J e. ( TopOn ` X ) )
iunconn.3 
|- ( ( ph /\ k e. A ) -> B C_ X )
iunconn.4 
|- ( ( ph /\ k e. A ) -> P e. B )
iunconn.5 
|- ( ( ph /\ k e. A ) -> ( J |`t B ) e. Conn )
Assertion iunconn 
|- ( ph -> ( J |`t U_ k e. A B ) e. Conn )

Proof

Step Hyp Ref Expression
1 iunconn.2 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 iunconn.3 
 |-  ( ( ph /\ k e. A ) -> B C_ X )
3 iunconn.4 
 |-  ( ( ph /\ k e. A ) -> P e. B )
4 iunconn.5 
 |-  ( ( ph /\ k e. A ) -> ( J |`t B ) e. Conn )
5 simpr 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> U_ k e. A B C_ ( u u. v ) )
6 simplr1 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> ( u i^i U_ k e. A B ) =/= (/) )
7 n0 
 |-  ( ( u i^i U_ k e. A B ) =/= (/) <-> E. v v e. ( u i^i U_ k e. A B ) )
8 elinel2 
 |-  ( v e. ( u i^i U_ k e. A B ) -> v e. U_ k e. A B )
9 eliun 
 |-  ( v e. U_ k e. A B <-> E. k e. A v e. B )
10 rexn0 
 |-  ( E. k e. A v e. B -> A =/= (/) )
11 9 10 sylbi 
 |-  ( v e. U_ k e. A B -> A =/= (/) )
12 8 11 syl 
 |-  ( v e. ( u i^i U_ k e. A B ) -> A =/= (/) )
13 12 exlimiv 
 |-  ( E. v v e. ( u i^i U_ k e. A B ) -> A =/= (/) )
14 7 13 sylbi 
 |-  ( ( u i^i U_ k e. A B ) =/= (/) -> A =/= (/) )
15 6 14 syl 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> A =/= (/) )
16 simplll 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> ph )
17 3 ralrimiva 
 |-  ( ph -> A. k e. A P e. B )
18 16 17 syl 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> A. k e. A P e. B )
19 r19.2z 
 |-  ( ( A =/= (/) /\ A. k e. A P e. B ) -> E. k e. A P e. B )
20 15 18 19 syl2anc 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> E. k e. A P e. B )
21 eliun 
 |-  ( P e. U_ k e. A B <-> E. k e. A P e. B )
22 20 21 sylibr 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> P e. U_ k e. A B )
23 5 22 sseldd 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> P e. ( u u. v ) )
24 elun 
 |-  ( P e. ( u u. v ) <-> ( P e. u \/ P e. v ) )
25 23 24 sylib 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> ( P e. u \/ P e. v ) )
26 16 1 syl 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> J e. ( TopOn ` X ) )
27 16 2 sylan 
 |-  ( ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) /\ k e. A ) -> B C_ X )
28 16 3 sylan 
 |-  ( ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) /\ k e. A ) -> P e. B )
29 16 4 sylan 
 |-  ( ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) /\ k e. A ) -> ( J |`t B ) e. Conn )
30 simpllr 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> ( u e. J /\ v e. J ) )
31 30 simpld 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> u e. J )
32 30 simprd 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> v e. J )
33 simplr2 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> ( v i^i U_ k e. A B ) =/= (/) )
34 simplr3 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> ( u i^i v ) C_ ( X \ U_ k e. A B ) )
35 nfv 
 |-  F/ k ( ph /\ ( u e. J /\ v e. J ) )
36 nfcv 
 |-  F/_ k u
37 nfiu1 
 |-  F/_ k U_ k e. A B
38 36 37 nfin 
 |-  F/_ k ( u i^i U_ k e. A B )
39 nfcv 
 |-  F/_ k (/)
40 38 39 nfne 
 |-  F/ k ( u i^i U_ k e. A B ) =/= (/)
41 nfcv 
 |-  F/_ k v
42 41 37 nfin 
 |-  F/_ k ( v i^i U_ k e. A B )
43 42 39 nfne 
 |-  F/ k ( v i^i U_ k e. A B ) =/= (/)
44 nfcv 
 |-  F/_ k ( u i^i v )
45 nfcv 
 |-  F/_ k X
46 45 37 nfdif 
 |-  F/_ k ( X \ U_ k e. A B )
47 44 46 nfss 
 |-  F/ k ( u i^i v ) C_ ( X \ U_ k e. A B )
48 40 43 47 nf3an 
 |-  F/ k ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) )
49 35 48 nfan 
 |-  F/ k ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) )
50 36 41 nfun 
 |-  F/_ k ( u u. v )
51 37 50 nfss 
 |-  F/ k U_ k e. A B C_ ( u u. v )
52 49 51 nfan 
 |-  F/ k ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) )
53 26 27 28 29 31 32 33 34 5 52 iunconnlem 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> -. P e. u )
54 incom 
 |-  ( v i^i u ) = ( u i^i v )
55 54 34 eqsstrid 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> ( v i^i u ) C_ ( X \ U_ k e. A B ) )
56 uncom 
 |-  ( u u. v ) = ( v u. u )
57 5 56 sseqtrdi 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> U_ k e. A B C_ ( v u. u ) )
58 26 27 28 29 32 31 6 55 57 52 iunconnlem 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> -. P e. v )
59 ioran 
 |-  ( -. ( P e. u \/ P e. v ) <-> ( -. P e. u /\ -. P e. v ) )
60 53 58 59 sylanbrc 
 |-  ( ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) /\ U_ k e. A B C_ ( u u. v ) ) -> -. ( P e. u \/ P e. v ) )
61 25 60 pm2.65da 
 |-  ( ( ( ph /\ ( u e. J /\ v e. J ) ) /\ ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) ) -> -. U_ k e. A B C_ ( u u. v ) )
62 61 ex 
 |-  ( ( ph /\ ( u e. J /\ v e. J ) ) -> ( ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) -> -. U_ k e. A B C_ ( u u. v ) ) )
63 62 ralrimivva 
 |-  ( ph -> A. u e. J A. v e. J ( ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) -> -. U_ k e. A B C_ ( u u. v ) ) )
64 2 ralrimiva 
 |-  ( ph -> A. k e. A B C_ X )
65 iunss 
 |-  ( U_ k e. A B C_ X <-> A. k e. A B C_ X )
66 64 65 sylibr 
 |-  ( ph -> U_ k e. A B C_ X )
67 connsub 
 |-  ( ( J e. ( TopOn ` X ) /\ U_ k e. A B C_ X ) -> ( ( J |`t U_ k e. A B ) e. Conn <-> A. u e. J A. v e. J ( ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) -> -. U_ k e. A B C_ ( u u. v ) ) ) )
68 1 66 67 syl2anc 
 |-  ( ph -> ( ( J |`t U_ k e. A B ) e. Conn <-> A. u e. J A. v e. J ( ( ( u i^i U_ k e. A B ) =/= (/) /\ ( v i^i U_ k e. A B ) =/= (/) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) -> -. U_ k e. A B C_ ( u u. v ) ) ) )
69 63 68 mpbird 
 |-  ( ph -> ( J |`t U_ k e. A B ) e. Conn )