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