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 
|- ( ps <-> ( ( ( ( ( ( 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 ) ) )
iunconnlem2.2 
|- ( ph -> J e. ( TopOn ` X ) )
iunconnlem2.3 
|- ( ( ph /\ k e. A ) -> B C_ X )
iunconnlem2.4 
|- ( ( ph /\ k e. A ) -> P e. B )
iunconnlem2.5 
|- ( ( ph /\ k e. A ) -> ( J |`t B ) e. Conn )
Assertion iunconnlem2 
|- ( ph -> ( J |`t U_ k e. A B ) e. Conn )

Proof

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