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 φJTopOnX
iunconn.3 φkABX
iunconn.4 φkAPB
iunconn.5 φkAJ𝑡BConn
Assertion iunconn φJ𝑡kABConn

Proof

Step Hyp Ref Expression
1 iunconn.2 φJTopOnX
2 iunconn.3 φkABX
3 iunconn.4 φkAPB
4 iunconn.5 φkAJ𝑡BConn
5 simpr φuJvJukABvkABuvXkABkABuvkABuv
6 simplr1 φuJvJukABvkABuvXkABkABuvukAB
7 n0 ukABvvukAB
8 elinel2 vukABvkAB
9 eliun vkABkAvB
10 rexn0 kAvBA
11 9 10 sylbi vkABA
12 8 11 syl vukABA
13 12 exlimiv vvukABA
14 7 13 sylbi ukABA
15 6 14 syl φuJvJukABvkABuvXkABkABuvA
16 simplll φuJvJukABvkABuvXkABkABuvφ
17 3 ralrimiva φkAPB
18 16 17 syl φuJvJukABvkABuvXkABkABuvkAPB
19 r19.2z AkAPBkAPB
20 15 18 19 syl2anc φuJvJukABvkABuvXkABkABuvkAPB
21 eliun PkABkAPB
22 20 21 sylibr φuJvJukABvkABuvXkABkABuvPkAB
23 5 22 sseldd φuJvJukABvkABuvXkABkABuvPuv
24 elun PuvPuPv
25 23 24 sylib φuJvJukABvkABuvXkABkABuvPuPv
26 16 1 syl φuJvJukABvkABuvXkABkABuvJTopOnX
27 16 2 sylan φuJvJukABvkABuvXkABkABuvkABX
28 16 3 sylan φuJvJukABvkABuvXkABkABuvkAPB
29 16 4 sylan φuJvJukABvkABuvXkABkABuvkAJ𝑡BConn
30 simpllr φuJvJukABvkABuvXkABkABuvuJvJ
31 30 simpld φuJvJukABvkABuvXkABkABuvuJ
32 30 simprd φuJvJukABvkABuvXkABkABuvvJ
33 simplr2 φuJvJukABvkABuvXkABkABuvvkAB
34 simplr3 φuJvJukABvkABuvXkABkABuvuvXkAB
35 nfv kφuJvJ
36 nfcv _ku
37 nfiu1 _kkAB
38 36 37 nfin _kukAB
39 nfcv _k
40 38 39 nfne kukAB
41 nfcv _kv
42 41 37 nfin _kvkAB
43 42 39 nfne kvkAB
44 nfcv _kuv
45 nfcv _kX
46 45 37 nfdif _kXkAB
47 44 46 nfss kuvXkAB
48 40 43 47 nf3an kukABvkABuvXkAB
49 35 48 nfan kφuJvJukABvkABuvXkAB
50 36 41 nfun _kuv
51 37 50 nfss kkABuv
52 49 51 nfan kφuJvJukABvkABuvXkABkABuv
53 26 27 28 29 31 32 33 34 5 52 iunconnlem φuJvJukABvkABuvXkABkABuv¬Pu
54 incom vu=uv
55 54 34 eqsstrid φuJvJukABvkABuvXkABkABuvvuXkAB
56 uncom uv=vu
57 5 56 sseqtrdi φuJvJukABvkABuvXkABkABuvkABvu
58 26 27 28 29 32 31 6 55 57 52 iunconnlem φuJvJukABvkABuvXkABkABuv¬Pv
59 ioran ¬PuPv¬Pu¬Pv
60 53 58 59 sylanbrc φuJvJukABvkABuvXkABkABuv¬PuPv
61 25 60 pm2.65da φuJvJukABvkABuvXkAB¬kABuv
62 61 ex φuJvJukABvkABuvXkAB¬kABuv
63 62 ralrimivva φuJvJukABvkABuvXkAB¬kABuv
64 2 ralrimiva φkABX
65 iunss kABXkABX
66 64 65 sylibr φkABX
67 connsub JTopOnXkABXJ𝑡kABConnuJvJukABvkABuvXkAB¬kABuv
68 1 66 67 syl2anc φJ𝑡kABConnuJvJukABvkABuvXkAB¬kABuv
69 63 68 mpbird φJ𝑡kABConn