Metamath Proof Explorer


Theorem iunconnlem2

Description: The indexed union of connected overlapping subspaces sharing a common point is connected. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/iunconlem2vd.html . As it is verified by the Metamath program, iunconnlem2 verifies https://us.metamath.org/other/completeusersproof/iunconlem2vd.html . (Contributed by Alan Sare, 22-Apr-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses iunconnlem2.1 ψ φ u J v J u k A B v k A B u v X k A B k A B u v
iunconnlem2.2 φ J TopOn X
iunconnlem2.3 φ k A B X
iunconnlem2.4 φ k A P B
iunconnlem2.5 φ k A J 𝑡 B Conn
Assertion iunconnlem2 φ J 𝑡 k A B Conn

Proof

Step Hyp Ref Expression
1 iunconnlem2.1 ψ φ u J v J u k A B v k A B u v X k A B k A B u v
2 iunconnlem2.2 φ J TopOn X
3 iunconnlem2.3 φ k A B X
4 iunconnlem2.4 φ k A P B
5 iunconnlem2.5 φ k A J 𝑡 B Conn
6 3 ex φ k A B X
7 6 ralrimiv φ k A B X
8 iunss k A B X k A B X
9 8 biimpri k A B X k A B X
10 7 9 syl φ k A B X
11 1 biimpi ψ φ u J v J u k A B v k A B u v X k A B k A B u v
12 11 simprd ψ k A B u v
13 simp-4r φ 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
14 11 13 syl ψ u k A B
15 n0 u k A B w w u k A B
16 15 biimpi u k A B w w u k A B
17 14 16 syl ψ w w u k A B
18 inss2 u k A B k A B
19 id w u k A B w u k A B
20 18 19 sseldi w u k A B w k A B
21 eliun w k A B k A w B
22 21 biimpi w k A B k A w B
23 20 22 syl w u k A B k A w B
24 rexn0 k A w B A
25 23 24 syl w u k A B A
26 25 exlimiv w w u k A B A
27 17 26 syl ψ A
28 nfv k φ u J
29 nfv k v J
30 28 29 nfan k φ u J v J
31 nfcv _ k u
32 nfiu1 _ k k A B
33 31 32 nfin _ k u k A B
34 nfcv _ k
35 33 34 nfne k u k A B
36 30 35 nfan k φ u J v J u k A B
37 nfcv _ k v
38 37 32 nfin _ k v k A B
39 38 34 nfne k v k A B
40 36 39 nfan k φ u J v J u k A B v k A B
41 nfcv _ k u v
42 nfcv _ k X
43 42 32 nfdif _ k X k A B
44 41 43 nfss k u v X k A B
45 40 44 nfan k φ u J v J u k A B v k A B u v X k A B
46 nfcv _ k u v
47 32 46 nfss k k A B u v
48 45 47 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
49 1 nfbii k ψ k φ u J v J u k A B v k A B u v X k A B k A B u v
50 48 49 mpbir k ψ
51 simp-6l φ u J v J u k A B v k A B u v X k A B k A B u v φ
52 11 51 syl ψ φ
53 52 4 sylan ψ k A P B
54 53 ex ψ k A P B
55 50 54 ralrimi ψ k A P B
56 r19.2z A k A P B k A P B
57 56 ancoms k A P B A k A P B
58 57 ancoms A k A P B k A P B
59 27 55 58 syl2anc ψ k A P B
60 eliun P k A B k A P B
61 60 biimpri k A P B P k A B
62 59 61 syl ψ P k A B
63 12 62 sseldd ψ P u v
64 elun P u v P u P v
65 64 biimpi P u v P u P v
66 63 65 syl ψ P u P v
67 1 66 sylbir φ 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
68 52 2 syl ψ J TopOn X
69 52 3 sylan ψ k A B X
70 52 5 sylan ψ k A J 𝑡 B Conn
71 simp-6r φ 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
72 11 71 syl ψ u J
73 simp-5r φ 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
74 11 73 syl ψ v J
75 simpllr φ 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
76 11 75 syl ψ v k A B
77 simplr φ 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
78 11 77 syl ψ u v X k A B
79 68 69 53 70 72 74 76 78 12 50 iunconnlem ψ ¬ P u
80 incom v u = u v
81 80 78 eqsstrid ψ v u X k A B
82 uncom v u = u v
83 12 82 sseqtrrdi ψ k A B v u
84 68 69 53 70 74 72 14 81 83 50 iunconnlem ψ ¬ P v
85 pm4.56 ¬ P u ¬ P v ¬ P u P v
86 85 biimpi ¬ P u ¬ P v ¬ P u P v
87 86 idiALT ¬ P u ¬ P v ¬ P u P v
88 79 84 87 syl2anc ψ ¬ P u P v
89 1 88 sylbir φ 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
90 67 89 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
91 90 ex φ u J v J u k A B v k A B u v X k A B ¬ k A B u v
92 91 ex φ u J v J u k A B v k A B u v X k A B ¬ k A B u v
93 92 ex3 φ u J v J u k A B v k A B u v X k A B ¬ k A B u v
94 93 3impd φ u J v J u k A B v k A B u v X k A B ¬ k A B u v
95 94 3expia φ u J v J u k A B v k A B u v X k A B ¬ k A B u v
96 95 ex φ u J v J u k A B v k A B u v X k A B ¬ k A B u v
97 96 impd φ u J v J u k A B v k A B u v X k A B ¬ k A B u v
98 97 ralrimivv φ u J v J u k A B v k A B u v X k A B ¬ k A B u v
99 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
100 99 biimp3ar J TopOn X k A B X u J v J u k A B v k A B u v X k A B ¬ k A B u v J 𝑡 k A B Conn
101 2 10 98 100 syl3anc φ J 𝑡 k A B Conn