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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) → ( 𝐽 ↾t ( 𝐴 ∪ 𝐵 ) ) ∈ Conn ) )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( ( 𝐴 ∩ 𝐵 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
2 uniiun ⊢ ∪ { 𝐴 , 𝐵 } = ∪ 𝑘 ∈ { 𝐴 , 𝐵 } 𝑘
3 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
5 3 4 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → 𝑋 ∈ 𝐽 )
6 simpl2l ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → 𝐴 ⊆ 𝑋 )
7 5 6 ssexd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → 𝐴 ∈ V )
8 simpl2r ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → 𝐵 ⊆ 𝑋 )
9 5 8 ssexd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → 𝐵 ∈ V )
10 uniprg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
11 7 9 10 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
12 2 11 eqtr3id ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → ∪ 𝑘 ∈ { 𝐴 , 𝐵 } 𝑘 = ( 𝐴 ∪ 𝐵 ) )
13 12 oveq2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → ( 𝐽 ↾t ∪ 𝑘 ∈ { 𝐴 , 𝐵 } 𝑘 ) = ( 𝐽 ↾t ( 𝐴 ∪ 𝐵 ) ) )
14 vex ⊢ 𝑘 ∈ V
15 14 elpr ⊢ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) )
16 simpl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) )
17 sseq1 ⊢ ( 𝑘 = 𝐴 → ( 𝑘 ⊆ 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
18 17 biimprd ⊢ ( 𝑘 = 𝐴 → ( 𝐴 ⊆ 𝑋 → 𝑘 ⊆ 𝑋 ) )
19 sseq1 ⊢ ( 𝑘 = 𝐵 → ( 𝑘 ⊆ 𝑋 ↔ 𝐵 ⊆ 𝑋 ) )
20 19 biimprd ⊢ ( 𝑘 = 𝐵 → ( 𝐵 ⊆ 𝑋 → 𝑘 ⊆ 𝑋 ) )
21 18 20 jaoa ⊢ ( ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) → ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → 𝑘 ⊆ 𝑋 ) )
22 16 21 mpan9 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) ∧ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) ) → 𝑘 ⊆ 𝑋 )
23 15 22 sylan2b ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) → 𝑘 ⊆ 𝑋 )
24 simpl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
25 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
26 24 25 sylib ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
27 eleq2 ⊢ ( 𝑘 = 𝐴 → ( 𝑥 ∈ 𝑘 ↔ 𝑥 ∈ 𝐴 ) )
28 27 biimprd ⊢ ( 𝑘 = 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑘 ) )
29 eleq2 ⊢ ( 𝑘 = 𝐵 → ( 𝑥 ∈ 𝑘 ↔ 𝑥 ∈ 𝐵 ) )
30 29 biimprd ⊢ ( 𝑘 = 𝐵 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑘 ) )
31 28 30 jaoa ⊢ ( ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝑘 ) )
32 26 31 mpan9 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) ∧ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) ) → 𝑥 ∈ 𝑘 )
33 15 32 sylan2b ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) → 𝑥 ∈ 𝑘 )
34 simpr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) )
35 oveq2 ⊢ ( 𝑘 = 𝐴 → ( 𝐽 ↾t 𝑘 ) = ( 𝐽 ↾t 𝐴 ) )
36 35 eleq1d ⊢ ( 𝑘 = 𝐴 → ( ( 𝐽 ↾t 𝑘 ) ∈ Conn ↔ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) )
37 36 biimprd ⊢ ( 𝑘 = 𝐴 → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn → ( 𝐽 ↾t 𝑘 ) ∈ Conn ) )
38 oveq2 ⊢ ( 𝑘 = 𝐵 → ( 𝐽 ↾t 𝑘 ) = ( 𝐽 ↾t 𝐵 ) )
39 38 eleq1d ⊢ ( 𝑘 = 𝐵 → ( ( 𝐽 ↾t 𝑘 ) ∈ Conn ↔ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) )
40 39 biimprd ⊢ ( 𝑘 = 𝐵 → ( ( 𝐽 ↾t 𝐵 ) ∈ Conn → ( 𝐽 ↾t 𝑘 ) ∈ Conn ) )
41 37 40 jaoa ⊢ ( ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) → ( ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) → ( 𝐽 ↾t 𝑘 ) ∈ Conn ) )
42 34 41 mpan9 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) ∧ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) ) → ( 𝐽 ↾t 𝑘 ) ∈ Conn )
43 15 42 sylan2b ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) → ( 𝐽 ↾t 𝑘 ) ∈ Conn )
44 3 23 33 43 iunconn ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → ( 𝐽 ↾t ∪ 𝑘 ∈ { 𝐴 , 𝐵 } 𝑘 ) ∈ Conn )
45 13 44 eqeltrrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) ) → ( 𝐽 ↾t ( 𝐴 ∪ 𝐵 ) ) ∈ Conn )
46 45 ex ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) → ( 𝐽 ↾t ( 𝐴 ∪ 𝐵 ) ) ∈ Conn ) )
47 46 3expia ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → ( ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) → ( 𝐽 ↾t ( 𝐴 ∪ 𝐵 ) ) ∈ Conn ) ) )
48 47 exlimdv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ) → ( ∃ 𝑥 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → ( ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) → ( 𝐽 ↾t ( 𝐴 ∪ 𝐵 ) ) ∈ Conn ) ) )
49 1 48 syl5bi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ) → ( ( 𝐴 ∩ 𝐵 ) ≠ ∅ → ( ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) → ( 𝐽 ↾t ( 𝐴 ∪ 𝐵 ) ) ∈ Conn ) ) )
50 49 3impia ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐽 ↾t 𝐵 ) ∈ Conn ) → ( 𝐽 ↾t ( 𝐴 ∪ 𝐵 ) ) ∈ Conn ) )