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 φ J TopOn X
iunconn.3 φ k A B X
iunconn.4 φ k A P B
iunconn.5 φ k A J 𝑡 B Conn
Assertion iunconn φ J 𝑡 k A B Conn

Proof

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