Metamath Proof Explorer

Theorem iunconnlem2

Description: The indexed union of connected overlapping subspaces sharing a common point is connected. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/iunconlem2vd.html . As it is verified by the Metamath program, iunconnlem2 verifies https://us.metamath.org/other/completeusersproof/iunconlem2vd.html . (Contributed by Alan Sare, 22-Apr-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses iunconnlem2.1 ⊢ ( 𝜓 ↔ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) )
iunconnlem2.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
iunconnlem2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 )
iunconnlem2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
iunconnlem2.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn )
Assertion iunconnlem2 ( 𝜑 → ( 𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵 ) ∈ Conn )

Proof

Step Hyp Ref Expression
1 iunconnlem2.1 ⊢ ( 𝜓 ↔ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) )
2 iunconnlem2.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 iunconnlem2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 )
4 iunconnlem2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
5 iunconnlem2.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn )
6 3 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝐵 ⊆ 𝑋 ) )
7 6 ralrimiv ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 )
8 iunss ⊢ ( ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 ↔ ∀ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 )
9 8 biimpri ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 )
10 7 9 syl ⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 )
11 1 biimpi ⊢ ( 𝜓 → ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) )
12 11 simprd ⊢ ( 𝜓 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) )
13 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ )
14 11 13 syl ⊢ ( 𝜓 → ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ )
15 n0 ⊢ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
16 15 biimpi ⊢ ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ → ∃ 𝑤 𝑤 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
17 14 16 syl ⊢ ( 𝜓 → ∃ 𝑤 𝑤 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
18 inss2 ⊢ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ⊆ ∪ 𝑘 ∈ 𝐴 𝐵
19 id ⊢ ( 𝑤 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) → 𝑤 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
20 18 19 sselid ⊢ ( 𝑤 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) → 𝑤 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 )
21 eliun ⊢ ( 𝑤 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 ↔ ∃ 𝑘 ∈ 𝐴 𝑤 ∈ 𝐵 )
22 21 biimpi ⊢ ( 𝑤 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 → ∃ 𝑘 ∈ 𝐴 𝑤 ∈ 𝐵 )
23 20 22 syl ⊢ ( 𝑤 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) → ∃ 𝑘 ∈ 𝐴 𝑤 ∈ 𝐵 )
24 rexn0 ⊢ ( ∃ 𝑘 ∈ 𝐴 𝑤 ∈ 𝐵 → 𝐴 ≠ ∅ )
25 23 24 syl ⊢ ( 𝑤 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) → 𝐴 ≠ ∅ )
26 25 exlimiv ⊢ ( ∃ 𝑤 𝑤 ∈ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) → 𝐴 ≠ ∅ )
27 17 26 syl ⊢ ( 𝜓 → 𝐴 ≠ ∅ )
28 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑢 ∈ 𝐽 )
29 nfv ⊢ Ⅎ 𝑘 𝑣 ∈ 𝐽
30 28 29 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 )
31 nfcv ⊢ Ⅎ 𝑘 𝑢
32 nfiu1 ⊢ Ⅎ 𝑘 ∪ 𝑘 ∈ 𝐴 𝐵
33 31 32 nfin ⊢ Ⅎ 𝑘 ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 )
34 nfcv ⊢ Ⅎ 𝑘 ∅
35 33 34 nfne ⊢ Ⅎ 𝑘 ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅
36 30 35 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ )
37 nfcv ⊢ Ⅎ 𝑘 𝑣
38 37 32 nfin ⊢ Ⅎ 𝑘 ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 )
39 38 34 nfne ⊢ Ⅎ 𝑘 ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅
40 36 39 nfan ⊢ Ⅎ 𝑘 ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ )
41 nfcv ⊢ Ⅎ 𝑘 ( 𝑢 ∩ 𝑣 )
42 nfcv ⊢ Ⅎ 𝑘 𝑋
43 42 32 nfdif ⊢ Ⅎ 𝑘 ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 )
44 41 43 nfss ⊢ Ⅎ 𝑘 ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 )
45 40 44 nfan ⊢ Ⅎ 𝑘 ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
46 nfcv ⊢ Ⅎ 𝑘 ( 𝑢 ∪ 𝑣 )
47 32 46 nfss ⊢ Ⅎ 𝑘 ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 )
48 45 47 nfan ⊢ Ⅎ 𝑘 ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) )
49 1 nfbii ⊢ ( Ⅎ 𝑘 𝜓 ↔ Ⅎ 𝑘 ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) )
50 48 49 mpbir ⊢ Ⅎ 𝑘 𝜓
51 simp-6l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → 𝜑 )
52 11 51 syl ⊢ ( 𝜓 → 𝜑 )
53 52 4 sylan ⊢ ( ( 𝜓 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
54 53 ex ⊢ ( 𝜓 → ( 𝑘 ∈ 𝐴 → 𝑃 ∈ 𝐵 ) )
55 50 54 ralrimi ⊢ ( 𝜓 → ∀ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
56 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 ) → ∃ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
57 56 ancoms ⊢ ( ( ∀ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
58 57 ancoms ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 ) → ∃ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
59 27 55 58 syl2anc ⊢ ( 𝜓 → ∃ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
60 eliun ⊢ ( 𝑃 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 ↔ ∃ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 )
61 60 biimpri ⊢ ( ∃ 𝑘 ∈ 𝐴 𝑃 ∈ 𝐵 → 𝑃 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 )
62 59 61 syl ⊢ ( 𝜓 → 𝑃 ∈ ∪ 𝑘 ∈ 𝐴 𝐵 )
63 12 62 sseldd ⊢ ( 𝜓 → 𝑃 ∈ ( 𝑢 ∪ 𝑣 ) )
64 elun ⊢ ( 𝑃 ∈ ( 𝑢 ∪ 𝑣 ) ↔ ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
65 64 biimpi ⊢ ( 𝑃 ∈ ( 𝑢 ∪ 𝑣 ) → ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
66 63 65 syl ⊢ ( 𝜓 → ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
67 1 66 sylbir ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
68 52 2 syl ⊢ ( 𝜓 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
69 52 3 sylan ⊢ ( ( 𝜓 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 )
70 52 5 sylan ⊢ ( ( 𝜓 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn )
71 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → 𝑢 ∈ 𝐽 )
72 11 71 syl ⊢ ( 𝜓 → 𝑢 ∈ 𝐽 )
73 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → 𝑣 ∈ 𝐽 )
74 11 73 syl ⊢ ( 𝜓 → 𝑣 ∈ 𝐽 )
75 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ )
76 11 75 syl ⊢ ( 𝜓 → ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ )
77 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
78 11 77 syl ⊢ ( 𝜓 → ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
79 68 69 53 70 72 74 76 78 12 50 iunconnlem ⊢ ( 𝜓 → ¬ 𝑃 ∈ 𝑢 )
80 incom ⊢ ( 𝑣 ∩ 𝑢 ) = ( 𝑢 ∩ 𝑣 )
81 80 78 eqsstrid ⊢ ( 𝜓 → ( 𝑣 ∩ 𝑢 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) )
82 uncom ⊢ ( 𝑣 ∪ 𝑢 ) = ( 𝑢 ∪ 𝑣 )
83 12 82 sseqtrrdi ⊢ ( 𝜓 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑣 ∪ 𝑢 ) )
84 68 69 53 70 74 72 14 81 83 50 iunconnlem ⊢ ( 𝜓 → ¬ 𝑃 ∈ 𝑣 )
85 pm4.56 ⊢ ( ( ¬ 𝑃 ∈ 𝑢 ∧ ¬ 𝑃 ∈ 𝑣 ) ↔ ¬ ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
86 85 biimpi ⊢ ( ( ¬ 𝑃 ∈ 𝑢 ∧ ¬ 𝑃 ∈ 𝑣 ) → ¬ ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
87 86 idiALT ⊢ ( ( ¬ 𝑃 ∈ 𝑢 ∧ ¬ 𝑃 ∈ 𝑣 ) → ¬ ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
88 79 84 87 syl2anc ⊢ ( 𝜓 → ¬ ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
89 1 88 sylbir ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) → ¬ ( 𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣 ) )
90 67 89 pm2.65da ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) )
91 90 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) → ( ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) )
92 91 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) → ( ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ → ( ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) )
93 92 ex3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) → ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ → ( ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ → ( ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) ) )
94 93 3impd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) → ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) )
95 94 3expia ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( 𝑣 ∈ 𝐽 → ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) )
96 95 ex ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐽 → ( 𝑣 ∈ 𝐽 → ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) ) )
97 96 impd ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) → ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) )
98 97 ralrimivv ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐽 ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) )
99 connsub ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 ) → ( ( 𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵 ) ∈ Conn ↔ ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐽 ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) )
100 99 biimp3ar ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐽 ( ( ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) → ¬ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) → ( 𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵 ) ∈ Conn )
101 2 10 98 100 syl3anc ⊢ ( 𝜑 → ( 𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵 ) ∈ Conn )