Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  iunconnlem2 Structured version   Visualization version   GIF version

Theorem iunconnlem2 40728
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 40728 verifies https://us.metamath.org/other/completeusersproof/iunconlem2vd.html. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
iunconnlem2.1 (𝜓 ↔ ((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))
iunconnlem2.2 (𝜑𝐽 ∈ (TopOn‘𝑋))
iunconnlem2.3 ((𝜑𝑘𝐴) → 𝐵𝑋)
iunconnlem2.4 ((𝜑𝑘𝐴) → 𝑃𝐵)
iunconnlem2.5 ((𝜑𝑘𝐴) → (𝐽t 𝐵) ∈ Conn)
Assertion
Ref Expression
iunconnlem2 (𝜑 → (𝐽t 𝑘𝐴 𝐵) ∈ Conn)
Distinct variable groups:   𝑢,𝑘,𝑣,𝜑   𝐴,𝑘,𝑢,𝑣   𝑢,𝐵,𝑣   𝑘,𝐽,𝑢,𝑣   𝑃,𝑘   𝑘,𝑋,𝑢,𝑣
Allowed substitution hints:   𝜓(𝑣,𝑢,𝑘)   𝐵(𝑘)   𝑃(𝑣,𝑢)

Proof of Theorem iunconnlem2
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 iunconnlem2.2 . 2 (𝜑𝐽 ∈ (TopOn‘𝑋))
2 iunconnlem2.3 . . . . 5 ((𝜑𝑘𝐴) → 𝐵𝑋)
32ex 405 . . . 4 (𝜑 → (𝑘𝐴𝐵𝑋))
43ralrimiv 3133 . . 3 (𝜑 → ∀𝑘𝐴 𝐵𝑋)
5 iunss 4840 . . . 4 ( 𝑘𝐴 𝐵𝑋 ↔ ∀𝑘𝐴 𝐵𝑋)
65biimpri 220 . . 3 (∀𝑘𝐴 𝐵𝑋 𝑘𝐴 𝐵𝑋)
74, 6syl 17 . 2 (𝜑 𝑘𝐴 𝐵𝑋)
8 iunconnlem2.1 . . . . . . . . . . . 12 (𝜓 ↔ ((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))
98biimpi 208 . . . . . . . . . . . . . . 15 (𝜓 → ((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))
109simprd 488 . . . . . . . . . . . . . 14 (𝜓 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))
11 simp-4r 772 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → (𝑢 𝑘𝐴 𝐵) ≠ ∅)
129, 11syl 17 . . . . . . . . . . . . . . . . . 18 (𝜓 → (𝑢 𝑘𝐴 𝐵) ≠ ∅)
13 n0 4199 . . . . . . . . . . . . . . . . . . 19 ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑢 𝑘𝐴 𝐵))
1413biimpi 208 . . . . . . . . . . . . . . . . . 18 ((𝑢 𝑘𝐴 𝐵) ≠ ∅ → ∃𝑤 𝑤 ∈ (𝑢 𝑘𝐴 𝐵))
1512, 14syl 17 . . . . . . . . . . . . . . . . 17 (𝜓 → ∃𝑤 𝑤 ∈ (𝑢 𝑘𝐴 𝐵))
16 inss2 4096 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 𝑘𝐴 𝐵) ⊆ 𝑘𝐴 𝐵
17 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (𝑢 𝑘𝐴 𝐵) → 𝑤 ∈ (𝑢 𝑘𝐴 𝐵))
1816, 17sseldi 3858 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑢 𝑘𝐴 𝐵) → 𝑤 𝑘𝐴 𝐵)
19 eliun 4801 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 𝑘𝐴 𝐵 ↔ ∃𝑘𝐴 𝑤𝐵)
2019biimpi 208 . . . . . . . . . . . . . . . . . . . 20 (𝑤 𝑘𝐴 𝐵 → ∃𝑘𝐴 𝑤𝐵)
2118, 20syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝑢 𝑘𝐴 𝐵) → ∃𝑘𝐴 𝑤𝐵)
22 rexn0 4340 . . . . . . . . . . . . . . . . . . 19 (∃𝑘𝐴 𝑤𝐵𝐴 ≠ ∅)
2321, 22syl 17 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (𝑢 𝑘𝐴 𝐵) → 𝐴 ≠ ∅)
2423exlimiv 1890 . . . . . . . . . . . . . . . . 17 (∃𝑤 𝑤 ∈ (𝑢 𝑘𝐴 𝐵) → 𝐴 ≠ ∅)
2515, 24syl 17 . . . . . . . . . . . . . . . 16 (𝜓𝐴 ≠ ∅)
26 nfv 1874 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(𝜑𝑢𝐽)
27 nfv 1874 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 𝑣𝐽
2826, 27nfan 1863 . . . . . . . . . . . . . . . . . . . . . 22 𝑘((𝜑𝑢𝐽) ∧ 𝑣𝐽)
29 nfcv 2934 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘𝑢
30 nfiu1 4828 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 𝑘𝐴 𝐵
3129, 30nfin 4083 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(𝑢 𝑘𝐴 𝐵)
32 nfcv 2934 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘
3331, 32nfne 3072 . . . . . . . . . . . . . . . . . . . . . 22 𝑘(𝑢 𝑘𝐴 𝐵) ≠ ∅
3428, 33nfan 1863 . . . . . . . . . . . . . . . . . . . . 21 𝑘(((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅)
35 nfcv 2934 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘𝑣
3635, 30nfin 4083 . . . . . . . . . . . . . . . . . . . . . 22 𝑘(𝑣 𝑘𝐴 𝐵)
3736, 32nfne 3072 . . . . . . . . . . . . . . . . . . . . 21 𝑘(𝑣 𝑘𝐴 𝐵) ≠ ∅
3834, 37nfan 1863 . . . . . . . . . . . . . . . . . . . 20 𝑘((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅)
39 nfcv 2934 . . . . . . . . . . . . . . . . . . . . 21 𝑘(𝑢𝑣)
40 nfcv 2934 . . . . . . . . . . . . . . . . . . . . . 22 𝑘𝑋
4140, 30nfdif 3994 . . . . . . . . . . . . . . . . . . . . 21 𝑘(𝑋 𝑘𝐴 𝐵)
4239, 41nfss 3853 . . . . . . . . . . . . . . . . . . . 20 𝑘(𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)
4338, 42nfan 1863 . . . . . . . . . . . . . . . . . . 19 𝑘(((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))
44 nfcv 2934 . . . . . . . . . . . . . . . . . . . 20 𝑘(𝑢𝑣)
4530, 44nfss 3853 . . . . . . . . . . . . . . . . . . 19 𝑘 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)
4643, 45nfan 1863 . . . . . . . . . . . . . . . . . 18 𝑘((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))
478nfbii 1815 . . . . . . . . . . . . . . . . . 18 (Ⅎ𝑘𝜓 ↔ Ⅎ𝑘((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))
4846, 47mpbir 223 . . . . . . . . . . . . . . . . 17 𝑘𝜓
49 simp-6l 775 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝜑)
509, 49syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜓𝜑)
51 iunconnlem2.4 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐴) → 𝑃𝐵)
5250, 51sylan 572 . . . . . . . . . . . . . . . . . 18 ((𝜓𝑘𝐴) → 𝑃𝐵)
5352ex 405 . . . . . . . . . . . . . . . . 17 (𝜓 → (𝑘𝐴𝑃𝐵))
5448, 53ralrimi 3168 . . . . . . . . . . . . . . . 16 (𝜓 → ∀𝑘𝐴 𝑃𝐵)
55 r19.2z 4326 . . . . . . . . . . . . . . . . . 18 ((𝐴 ≠ ∅ ∧ ∀𝑘𝐴 𝑃𝐵) → ∃𝑘𝐴 𝑃𝐵)
5655ancoms 451 . . . . . . . . . . . . . . . . 17 ((∀𝑘𝐴 𝑃𝐵𝐴 ≠ ∅) → ∃𝑘𝐴 𝑃𝐵)
5756ancoms 451 . . . . . . . . . . . . . . . 16 ((𝐴 ≠ ∅ ∧ ∀𝑘𝐴 𝑃𝐵) → ∃𝑘𝐴 𝑃𝐵)
5825, 54, 57syl2anc 576 . . . . . . . . . . . . . . 15 (𝜓 → ∃𝑘𝐴 𝑃𝐵)
59 eliun 4801 . . . . . . . . . . . . . . . 16 (𝑃 𝑘𝐴 𝐵 ↔ ∃𝑘𝐴 𝑃𝐵)
6059biimpri 220 . . . . . . . . . . . . . . 15 (∃𝑘𝐴 𝑃𝐵𝑃 𝑘𝐴 𝐵)
6158, 60syl 17 . . . . . . . . . . . . . 14 (𝜓𝑃 𝑘𝐴 𝐵)
6210, 61sseldd 3861 . . . . . . . . . . . . 13 (𝜓𝑃 ∈ (𝑢𝑣))
63 elun 4016 . . . . . . . . . . . . . 14 (𝑃 ∈ (𝑢𝑣) ↔ (𝑃𝑢𝑃𝑣))
6463biimpi 208 . . . . . . . . . . . . 13 (𝑃 ∈ (𝑢𝑣) → (𝑃𝑢𝑃𝑣))
6562, 64syl 17 . . . . . . . . . . . 12 (𝜓 → (𝑃𝑢𝑃𝑣))
668, 65sylbir 227 . . . . . . . . . . 11 (((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → (𝑃𝑢𝑃𝑣))
6750, 1syl 17 . . . . . . . . . . . . . 14 (𝜓𝐽 ∈ (TopOn‘𝑋))
6850, 2sylan 572 . . . . . . . . . . . . . 14 ((𝜓𝑘𝐴) → 𝐵𝑋)
69 iunconnlem2.5 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → (𝐽t 𝐵) ∈ Conn)
7050, 69sylan 572 . . . . . . . . . . . . . 14 ((𝜓𝑘𝐴) → (𝐽t 𝐵) ∈ Conn)
71 simp-6r 776 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝑢𝐽)
729, 71syl 17 . . . . . . . . . . . . . 14 (𝜓𝑢𝐽)
73 simp-5r 774 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝑣𝐽)
749, 73syl 17 . . . . . . . . . . . . . 14 (𝜓𝑣𝐽)
75 simpllr 764 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → (𝑣 𝑘𝐴 𝐵) ≠ ∅)
769, 75syl 17 . . . . . . . . . . . . . 14 (𝜓 → (𝑣 𝑘𝐴 𝐵) ≠ ∅)
77 simplr 757 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))
789, 77syl 17 . . . . . . . . . . . . . 14 (𝜓 → (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))
7967, 68, 52, 70, 72, 74, 76, 78, 10, 48iunconnlem 21754 . . . . . . . . . . . . 13 (𝜓 → ¬ 𝑃𝑢)
80 incom 4069 . . . . . . . . . . . . . . 15 (𝑣𝑢) = (𝑢𝑣)
8180, 78syl5eqss 3907 . . . . . . . . . . . . . 14 (𝜓 → (𝑣𝑢) ⊆ (𝑋 𝑘𝐴 𝐵))
82 uncom 4020 . . . . . . . . . . . . . . 15 (𝑣𝑢) = (𝑢𝑣)
8310, 82syl6sseqr 3910 . . . . . . . . . . . . . 14 (𝜓 𝑘𝐴 𝐵 ⊆ (𝑣𝑢))
8467, 68, 52, 70, 74, 72, 12, 81, 83, 48iunconnlem 21754 . . . . . . . . . . . . 13 (𝜓 → ¬ 𝑃𝑣)
85 pm4.56 972 . . . . . . . . . . . . . . 15 ((¬ 𝑃𝑢 ∧ ¬ 𝑃𝑣) ↔ ¬ (𝑃𝑢𝑃𝑣))
8685biimpi 208 . . . . . . . . . . . . . 14 ((¬ 𝑃𝑢 ∧ ¬ 𝑃𝑣) → ¬ (𝑃𝑢𝑃𝑣))
8786idiALT 40270 . . . . . . . . . . . . 13 ((¬ 𝑃𝑢 ∧ ¬ 𝑃𝑣) → ¬ (𝑃𝑢𝑃𝑣))
8879, 84, 87syl2anc 576 . . . . . . . . . . . 12 (𝜓 → ¬ (𝑃𝑢𝑃𝑣))
898, 88sylbir 227 . . . . . . . . . . 11 (((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → ¬ (𝑃𝑢𝑃𝑣))
9066, 89pm2.65da 805 . . . . . . . . . 10 ((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))
9190ex 405 . . . . . . . . 9 (((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅) → ((𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))
9291ex 405 . . . . . . . 8 ((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴 𝐵) ≠ ∅) → ((𝑣 𝑘𝐴 𝐵) ≠ ∅ → ((𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))))
9392ex3 1327 . . . . . . 7 ((𝜑𝑢𝐽𝑣𝐽) → ((𝑢 𝑘𝐴 𝐵) ≠ ∅ → ((𝑣 𝑘𝐴 𝐵) ≠ ∅ → ((𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))))
94933impd 1329 . . . . . 6 ((𝜑𝑢𝐽𝑣𝐽) → (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))
95943expia 1102 . . . . 5 ((𝜑𝑢𝐽) → (𝑣𝐽 → (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))))
9695ex 405 . . . 4 (𝜑 → (𝑢𝐽 → (𝑣𝐽 → (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))))
9796impd 402 . . 3 (𝜑 → ((𝑢𝐽𝑣𝐽) → (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))))
9897ralrimivv 3142 . 2 (𝜑 → ∀𝑢𝐽𝑣𝐽 (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))
99 connsub 21748 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑘𝐴 𝐵𝑋) → ((𝐽t 𝑘𝐴 𝐵) ∈ Conn ↔ ∀𝑢𝐽𝑣𝐽 (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))))
10099biimp3ar 1450 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑘𝐴 𝐵𝑋 ∧ ∀𝑢𝐽𝑣𝐽 (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))) → (𝐽t 𝑘𝐴 𝐵) ∈ Conn)
1011, 7, 98, 100syl3anc 1352 1 (𝜑 → (𝐽t 𝑘𝐴 𝐵) ∈ Conn)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 834  w3a 1069  wex 1743  wnf 1747  wcel 2051  wne 2969  wral 3090  wrex 3091  cdif 3828  cun 3829  cin 3830  wss 3831  c0 4181   ciun 4797  cfv 6193  (class class class)co 6982  t crest 16556  TopOnctopon 21237  Conncconn 21738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-rep 5053  ax-sep 5064  ax-nul 5071  ax-pow 5123  ax-pr 5190  ax-un 7285
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3419  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4182  df-if 4354  df-pw 4427  df-sn 4445  df-pr 4447  df-tp 4449  df-op 4451  df-uni 4718  df-int 4755  df-iun 4799  df-br 4935  df-opab 4997  df-mpt 5014  df-tr 5036  df-id 5316  df-eprel 5321  df-po 5330  df-so 5331  df-fr 5370  df-we 5372  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-pred 5991  df-ord 6037  df-on 6038  df-lim 6039  df-suc 6040  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-f1 6198  df-fo 6199  df-f1o 6200  df-fv 6201  df-ov 6985  df-oprab 6986  df-mpo 6987  df-om 7403  df-1st 7507  df-2nd 7508  df-wrecs 7756  df-recs 7818  df-rdg 7856  df-oadd 7915  df-er 8095  df-en 8313  df-fin 8316  df-fi 8676  df-rest 16558  df-topgen 16579  df-top 21221  df-topon 21238  df-bases 21273  df-cld 21346  df-conn 21739
This theorem is referenced by:  iunconnALT  40729
  Copyright terms: Public domain W3C validator