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 ) )