This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunconn

Description: The indexed union of connected overlapping subspaces sharing a common point is connected. (Contributed by Mario Carneiro, 11-Jun-2014)

Ref Expression
Hypotheses iunconn.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
iunconn.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 )
iunconn.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
iunconn.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn )
Assertion iunconn ( 𝜑 → ( 𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵 ) ∈ Conn )

Proof

Step Hyp Ref Expression
1 iunconn.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 iunconn.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 )
3 iunconn.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
4 iunconn.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn )
5 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) )
6 simplr1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ )
7 n0 ⊢ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
8 elinel2 ⊢ ( 𝑣 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) → 𝑣 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 )
9 eliun ⊢ ( 𝑣 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 ↔ ∃ 𝑘 ∈ 𝐴 𝑣 ∈ 𝐵 )
10 rexn0 ⊢ ( ∃ 𝑘 ∈ 𝐴 𝑣 ∈ 𝐵 → 𝐴 ≠ ∅ )
11 9 10 sylbi ⊢ ( 𝑣 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 → 𝐴 ≠ ∅ )
12 8 11 syl ⊢ ( 𝑣 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) → 𝐴 ≠ ∅ )
13 12 exlimiv ⊢ ( ∃ 𝑣 𝑣 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) → 𝐴 ≠ ∅ )
14 7 13 sylbi ⊢ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ → 𝐴 ≠ ∅ )
15 6 14 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → 𝐴 ≠ ∅ )
16 simplll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → 𝜑 )
17 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
18 16 17 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ∀ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
19 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 ) → ∃ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
20 15 18 19 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ∃ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
21 eliun ⊢ ( 𝑃 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 ↔ ∃ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
22 20 21 sylibr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → 𝑃 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 )
23 5 22 sseldd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → 𝑃 ∈ ( 𝑢 ∪ 𝑣 ) )
24 elun ⊢ ( 𝑃 ∈ ( 𝑢 ∪ 𝑣 ) ↔ ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
25 23 24 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
26 16 1 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
27 16 2 sylan ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 )
28 16 3 sylan ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
29 16 4 sylan ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn )
30 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) )
31 30 simpld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → 𝑢 ∈ 𝐽 )
32 30 simprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → 𝑣 ∈ 𝐽 )
33 simplr2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ )
34 simplr3 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
35 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) )
36 nfcv ⊢ Ⅎ 𝑘 𝑢
37 nfiu1 ⊢ Ⅎ 𝑘 ∪ 𝑘 ∈ 𝐴 𝐵
38 36 37 nfin ⊢ Ⅎ 𝑘 ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 )
39 nfcv ⊢ Ⅎ 𝑘 ∅
40 38 39 nfne ⊢ Ⅎ 𝑘 ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅
41 nfcv ⊢ Ⅎ 𝑘 𝑣
42 41 37 nfin ⊢ Ⅎ 𝑘 ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 )
43 42 39 nfne ⊢ Ⅎ 𝑘 ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅
44 nfcv ⊢ Ⅎ 𝑘 ( 𝑢 ∩ 𝑣 )
45 nfcv ⊢ Ⅎ 𝑘 𝑋
46 45 37 nfdif ⊢ Ⅎ 𝑘 ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 )
47 44 46 nfss ⊢ Ⅎ 𝑘 ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 )
48 40 43 47 nf3an ⊢ Ⅎ 𝑘 ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
49 35 48 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) )
50 36 41 nfun ⊢ Ⅎ 𝑘 ( 𝑢 ∪ 𝑣 )
51 37 50 nfss ⊢ Ⅎ 𝑘 ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 )
52 49 51 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) )
53 26 27 28 29 31 32 33 34 5 52 iunconnlem ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ¬ 𝑃 ∈ 𝑢 )
54 incom ⊢ ( 𝑣 ∩ 𝑢 ) = ( 𝑢 ∩ 𝑣 )
55 54 34 eqsstrid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ( 𝑣 ∩ 𝑢 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
56 uncom ⊢ ( 𝑢 ∪ 𝑣 ) = ( 𝑣 ∪ 𝑢 )
57 5 56 sseqtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑣 ∪ 𝑢 ) )
58 26 27 28 29 32 31 6 55 57 52 iunconnlem ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ¬ 𝑃 ∈ 𝑣 )
59 ioran ⊢ ( ¬ ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) ↔ ( ¬ 𝑃 ∈ 𝑢 ∧ ¬ 𝑃 ∈ 𝑣 ) )
60 53 58 59 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ¬ ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
61 25 60 pm2.65da ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) )
62 61 ex ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) → ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) )
63 62 ralrimivva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐽 ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) )
64 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 )
65 iunss ⊢ ( ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 ↔ ∀ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 )
66 64 65 sylibr ⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 )
67 connsub ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 ) → ( ( 𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵 ) ∈ Conn ↔ ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐽 ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) )
68 1 66 67 syl2anc ⊢ ( 𝜑 → ( ( 𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵 ) ∈ Conn ↔ ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐽 ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) )
69 63 68 mpbird ⊢ ( 𝜑 → ( 𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵 ) ∈ Conn )