Metamath Proof Explorer

Theorem connsuba

Description: Connectedness for a subspace. See connsub . (Contributed by FL, 29-May-2014) (Proof shortened by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion connsuba ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
2 dfconn2 ⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑢 ∈ ( 𝐽 ↾t 𝐴 ) ∀ 𝑣 ∈ ( 𝐽 ↾t 𝐴 ) ( ( 𝑢 ≠ ∅ ∧ 𝑣 ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ( 𝑢 ∪ 𝑣 ) ≠ 𝐴 ) ) )
3 1 2 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑢 ∈ ( 𝐽 ↾t 𝐴 ) ∀ 𝑣 ∈ ( 𝐽 ↾t 𝐴 ) ( ( 𝑢 ≠ ∅ ∧ 𝑣 ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ( 𝑢 ∪ 𝑣 ) ≠ 𝐴 ) ) )
4 vex ⊢ 𝑥 ∈ V
5 4 inex1 ⊢ ( 𝑥 ∩ 𝐴 ) ∈ V
6 5 a1i ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∩ 𝐴 ) ∈ V )
7 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
8 7 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝑋 ∈ 𝐽 )
9 simpr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 )
10 8 9 ssexd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V )
11 elrest ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ V ) → ( 𝑢 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐽 𝑢 = ( 𝑥 ∩ 𝐴 ) ) )
12 10 11 syldan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑢 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐽 𝑢 = ( 𝑥 ∩ 𝐴 ) ) )
13 vex ⊢ 𝑦 ∈ V
14 13 inex1 ⊢ ( 𝑦 ∩ 𝐴 ) ∈ V
15 14 a1i ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑦 ∩ 𝐴 ) ∈ V )
16 elrest ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ V ) → ( 𝑣 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐽 𝑣 = ( 𝑦 ∩ 𝐴 ) ) )
17 10 16 syldan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑣 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐽 𝑣 = ( 𝑦 ∩ 𝐴 ) ) )
18 17 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) → ( 𝑣 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐽 𝑣 = ( 𝑦 ∩ 𝐴 ) ) )
19 simplr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → 𝑢 = ( 𝑥 ∩ 𝐴 ) )
20 19 neeq1d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → ( 𝑢 ≠ ∅ ↔ ( 𝑥 ∩ 𝐴 ) ≠ ∅ ) )
21 simpr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → 𝑣 = ( 𝑦 ∩ 𝐴 ) )
22 21 neeq1d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → ( 𝑣 ≠ ∅ ↔ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ) )
23 19 21 ineq12d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → ( 𝑢 ∩ 𝑣 ) = ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑦 ∩ 𝐴 ) ) )
24 inindir ⊢ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑦 ∩ 𝐴 ) )
25 23 24 eqtr4di ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → ( 𝑢 ∩ 𝑣 ) = ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) )
26 25 eqeq1d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) )
27 20 22 26 3anbi123d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → ( ( 𝑢 ≠ ∅ ∧ 𝑣 ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ↔ ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) ) )
28 19 21 uneq12d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → ( 𝑢 ∪ 𝑣 ) = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑦 ∩ 𝐴 ) ) )
29 indir ⊢ ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑦 ∩ 𝐴 ) )
30 28 29 eqtr4di ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → ( 𝑢 ∪ 𝑣 ) = ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) )
31 30 neeq1d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → ( ( 𝑢 ∪ 𝑣 ) ≠ 𝐴 ↔ ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) )
32 27 31 imbi12d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) ∧ 𝑣 = ( 𝑦 ∩ 𝐴 ) ) → ( ( ( 𝑢 ≠ ∅ ∧ 𝑣 ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ( 𝑢 ∪ 𝑣 ) ≠ 𝐴 ) ↔ ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) )
33 15 18 32 ralxfr2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑢 = ( 𝑥 ∩ 𝐴 ) ) → ( ∀ 𝑣 ∈ ( 𝐽 ↾t 𝐴 ) ( ( 𝑢 ≠ ∅ ∧ 𝑣 ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ( 𝑢 ∪ 𝑣 ) ≠ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) )
34 6 12 33 ralxfr2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ∀ 𝑢 ∈ ( 𝐽 ↾t 𝐴 ) ∀ 𝑣 ∈ ( 𝐽 ↾t 𝐴 ) ( ( 𝑢 ≠ ∅ ∧ 𝑣 ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ( 𝑢 ∪ 𝑣 ) ≠ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) )
35 3 34 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) )