Metamath Proof Explorer

Theorem unconn

Description: The union of two connected overlapping subspaces is connected. (Contributed by FL, 29-May-2014) (Proof shortened by Mario Carneiro, 11-Jun-2014)

Ref Expression
Assertion unconn 
|- ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ ( A i^i B ) =/= (/) ) -> ( ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) -> ( J |`t ( A u. B ) ) e. Conn ) )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( ( A i^i B ) =/= (/) <-> E. x x e. ( A i^i B ) )
2 uniiun 
 |-  U. { A , B } = U_ k e. { A , B } k
3 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> J e. ( TopOn ` X ) )
4 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
5 3 4 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> X e. J )
6 simpl2l 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> A C_ X )
7 5 6 ssexd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> A e. _V )
8 simpl2r 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> B C_ X )
9 5 8 ssexd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> B e. _V )
10 uniprg 
 |-  ( ( A e. _V /\ B e. _V ) -> U. { A , B } = ( A u. B ) )
11 7 9 10 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> U. { A , B } = ( A u. B ) )
12 2 11 eqtr3id 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> U_ k e. { A , B } k = ( A u. B ) )
13 12 oveq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> ( J |`t U_ k e. { A , B } k ) = ( J |`t ( A u. B ) ) )
14 vex 
 |-  k e. _V
15 14 elpr 
 |-  ( k e. { A , B } <-> ( k = A \/ k = B ) )
16 simpl2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> ( A C_ X /\ B C_ X ) )
17 sseq1 
 |-  ( k = A -> ( k C_ X <-> A C_ X ) )
18 17 biimprd 
 |-  ( k = A -> ( A C_ X -> k C_ X ) )
19 sseq1 
 |-  ( k = B -> ( k C_ X <-> B C_ X ) )
20 19 biimprd 
 |-  ( k = B -> ( B C_ X -> k C_ X ) )
21 18 20 jaoa 
 |-  ( ( k = A \/ k = B ) -> ( ( A C_ X /\ B C_ X ) -> k C_ X ) )
22 16 21 mpan9 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) /\ ( k = A \/ k = B ) ) -> k C_ X )
23 15 22 sylan2b 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) /\ k e. { A , B } ) -> k C_ X )
24 simpl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> x e. ( A i^i B ) )
25 elin 
 |-  ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
26 24 25 sylib 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> ( x e. A /\ x e. B ) )
27 eleq2 
 |-  ( k = A -> ( x e. k <-> x e. A ) )
28 27 biimprd 
 |-  ( k = A -> ( x e. A -> x e. k ) )
29 eleq2 
 |-  ( k = B -> ( x e. k <-> x e. B ) )
30 29 biimprd 
 |-  ( k = B -> ( x e. B -> x e. k ) )
31 28 30 jaoa 
 |-  ( ( k = A \/ k = B ) -> ( ( x e. A /\ x e. B ) -> x e. k ) )
32 26 31 mpan9 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) /\ ( k = A \/ k = B ) ) -> x e. k )
33 15 32 sylan2b 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) /\ k e. { A , B } ) -> x e. k )
34 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) )
35 oveq2 
 |-  ( k = A -> ( J |`t k ) = ( J |`t A ) )
36 35 eleq1d 
 |-  ( k = A -> ( ( J |`t k ) e. Conn <-> ( J |`t A ) e. Conn ) )
37 36 biimprd 
 |-  ( k = A -> ( ( J |`t A ) e. Conn -> ( J |`t k ) e. Conn ) )
38 oveq2 
 |-  ( k = B -> ( J |`t k ) = ( J |`t B ) )
39 38 eleq1d 
 |-  ( k = B -> ( ( J |`t k ) e. Conn <-> ( J |`t B ) e. Conn ) )
40 39 biimprd 
 |-  ( k = B -> ( ( J |`t B ) e. Conn -> ( J |`t k ) e. Conn ) )
41 37 40 jaoa 
 |-  ( ( k = A \/ k = B ) -> ( ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) -> ( J |`t k ) e. Conn ) )
42 34 41 mpan9 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) /\ ( k = A \/ k = B ) ) -> ( J |`t k ) e. Conn )
43 15 42 sylan2b 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) /\ k e. { A , B } ) -> ( J |`t k ) e. Conn )
44 3 23 33 43 iunconn 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> ( J |`t U_ k e. { A , B } k ) e. Conn )
45 13 44 eqeltrrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) /\ ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) ) -> ( J |`t ( A u. B ) ) e. Conn )
46 45 ex 
 |-  ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ x e. ( A i^i B ) ) -> ( ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) -> ( J |`t ( A u. B ) ) e. Conn ) )
47 46 3expia 
 |-  ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) ) -> ( x e. ( A i^i B ) -> ( ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) -> ( J |`t ( A u. B ) ) e. Conn ) ) )
48 47 exlimdv 
 |-  ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) ) -> ( E. x x e. ( A i^i B ) -> ( ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) -> ( J |`t ( A u. B ) ) e. Conn ) ) )
49 1 48 syl5bi 
 |-  ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) ) -> ( ( A i^i B ) =/= (/) -> ( ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) -> ( J |`t ( A u. B ) ) e. Conn ) ) )
50 49 3impia 
 |-  ( ( J e. ( TopOn ` X ) /\ ( A C_ X /\ B C_ X ) /\ ( A i^i B ) =/= (/) ) -> ( ( ( J |`t A ) e. Conn /\ ( J |`t B ) e. Conn ) -> ( J |`t ( A u. B ) ) e. Conn ) )