Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunconn Structured version   Visualization version   GIF version

Theorem iunconn 21212
 Description: The indexed union of connected overlapping subspaces sharing a common point is connected. (Contributed by Mario Carneiro, 11-Jun-2014.)
Hypotheses
Ref Expression
iunconn.2 (𝜑𝐽 ∈ (TopOn‘𝑋))
iunconn.3 ((𝜑𝑘𝐴) → 𝐵𝑋)
iunconn.4 ((𝜑𝑘𝐴) → 𝑃𝐵)
iunconn.5 ((𝜑𝑘𝐴) → (𝐽t 𝐵) ∈ Conn)
Assertion
Ref Expression
iunconn (𝜑 → (𝐽t 𝑘𝐴 𝐵) ∈ Conn)
Distinct variable groups:   𝐴,𝑘   𝑘,𝐽   𝑃,𝑘   𝑘,𝑋   𝜑,𝑘
Allowed substitution hint:   𝐵(𝑘)

Proof of Theorem iunconn
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 477 . . . . . . 7 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))
2 simplr1 1101 . . . . . . . . . 10 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → (𝑢 𝑘𝐴 𝐵) ≠ ∅)
3 n0 3923 . . . . . . . . . . 11 ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ (𝑢 𝑘𝐴 𝐵))
4 inss2 3826 . . . . . . . . . . . . . 14 (𝑢 𝑘𝐴 𝐵) ⊆ 𝑘𝐴 𝐵
54sseli 3591 . . . . . . . . . . . . 13 (𝑣 ∈ (𝑢 𝑘𝐴 𝐵) → 𝑣 𝑘𝐴 𝐵)
6 eliun 4515 . . . . . . . . . . . . . 14 (𝑣 𝑘𝐴 𝐵 ↔ ∃𝑘𝐴 𝑣𝐵)
7 rexn0 4065 . . . . . . . . . . . . . 14 (∃𝑘𝐴 𝑣𝐵𝐴 ≠ ∅)
86, 7sylbi 207 . . . . . . . . . . . . 13 (𝑣 𝑘𝐴 𝐵𝐴 ≠ ∅)
95, 8syl 17 . . . . . . . . . . . 12 (𝑣 ∈ (𝑢 𝑘𝐴 𝐵) → 𝐴 ≠ ∅)
109exlimiv 1856 . . . . . . . . . . 11 (∃𝑣 𝑣 ∈ (𝑢 𝑘𝐴 𝐵) → 𝐴 ≠ ∅)
113, 10sylbi 207 . . . . . . . . . 10 ((𝑢 𝑘𝐴 𝐵) ≠ ∅ → 𝐴 ≠ ∅)
122, 11syl 17 . . . . . . . . 9 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝐴 ≠ ∅)
13 simplll 797 . . . . . . . . . 10 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝜑)
14 iunconn.4 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → 𝑃𝐵)
1514ralrimiva 2963 . . . . . . . . . 10 (𝜑 → ∀𝑘𝐴 𝑃𝐵)
1613, 15syl 17 . . . . . . . . 9 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → ∀𝑘𝐴 𝑃𝐵)
17 r19.2z 4051 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ ∀𝑘𝐴 𝑃𝐵) → ∃𝑘𝐴 𝑃𝐵)
1812, 16, 17syl2anc 692 . . . . . . . 8 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → ∃𝑘𝐴 𝑃𝐵)
19 eliun 4515 . . . . . . . 8 (𝑃 𝑘𝐴 𝐵 ↔ ∃𝑘𝐴 𝑃𝐵)
2018, 19sylibr 224 . . . . . . 7 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝑃 𝑘𝐴 𝐵)
211, 20sseldd 3596 . . . . . 6 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝑃 ∈ (𝑢𝑣))
22 elun 3745 . . . . . 6 (𝑃 ∈ (𝑢𝑣) ↔ (𝑃𝑢𝑃𝑣))
2321, 22sylib 208 . . . . 5 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → (𝑃𝑢𝑃𝑣))
24 iunconn.2 . . . . . . . 8 (𝜑𝐽 ∈ (TopOn‘𝑋))
2513, 24syl 17 . . . . . . 7 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝐽 ∈ (TopOn‘𝑋))
26 iunconn.3 . . . . . . . 8 ((𝜑𝑘𝐴) → 𝐵𝑋)
2713, 26sylan 488 . . . . . . 7 (((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) ∧ 𝑘𝐴) → 𝐵𝑋)
2813, 14sylan 488 . . . . . . 7 (((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) ∧ 𝑘𝐴) → 𝑃𝐵)
29 iunconn.5 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝐽t 𝐵) ∈ Conn)
3013, 29sylan 488 . . . . . . 7 (((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) ∧ 𝑘𝐴) → (𝐽t 𝐵) ∈ Conn)
31 simpllr 798 . . . . . . . 8 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → (𝑢𝐽𝑣𝐽))
3231simpld 475 . . . . . . 7 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝑢𝐽)
3331simprd 479 . . . . . . 7 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝑣𝐽)
34 simplr2 1102 . . . . . . 7 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → (𝑣 𝑘𝐴 𝐵) ≠ ∅)
35 simplr3 1103 . . . . . . 7 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))
36 nfv 1841 . . . . . . . . 9 𝑘(𝜑 ∧ (𝑢𝐽𝑣𝐽))
37 nfcv 2762 . . . . . . . . . . . 12 𝑘𝑢
38 nfiu1 4541 . . . . . . . . . . . 12 𝑘 𝑘𝐴 𝐵
3937, 38nfin 3812 . . . . . . . . . . 11 𝑘(𝑢 𝑘𝐴 𝐵)
40 nfcv 2762 . . . . . . . . . . 11 𝑘
4139, 40nfne 2891 . . . . . . . . . 10 𝑘(𝑢 𝑘𝐴 𝐵) ≠ ∅
42 nfcv 2762 . . . . . . . . . . . 12 𝑘𝑣
4342, 38nfin 3812 . . . . . . . . . . 11 𝑘(𝑣 𝑘𝐴 𝐵)
4443, 40nfne 2891 . . . . . . . . . 10 𝑘(𝑣 𝑘𝐴 𝐵) ≠ ∅
45 nfcv 2762 . . . . . . . . . . 11 𝑘(𝑢𝑣)
46 nfcv 2762 . . . . . . . . . . . 12 𝑘𝑋
4746, 38nfdif 3723 . . . . . . . . . . 11 𝑘(𝑋 𝑘𝐴 𝐵)
4845, 47nfss 3588 . . . . . . . . . 10 𝑘(𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)
4941, 44, 48nf3an 1829 . . . . . . . . 9 𝑘((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))
5036, 49nfan 1826 . . . . . . . 8 𝑘((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)))
5137, 42nfun 3761 . . . . . . . . 9 𝑘(𝑢𝑣)
5238, 51nfss 3588 . . . . . . . 8 𝑘 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)
5350, 52nfan 1826 . . . . . . 7 𝑘(((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))
5425, 27, 28, 30, 32, 33, 34, 35, 1, 53iunconnlem 21211 . . . . . 6 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → ¬ 𝑃𝑢)
55 incom 3797 . . . . . . . 8 (𝑣𝑢) = (𝑢𝑣)
5655, 35syl5eqss 3641 . . . . . . 7 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → (𝑣𝑢) ⊆ (𝑋 𝑘𝐴 𝐵))
57 uncom 3749 . . . . . . . 8 (𝑢𝑣) = (𝑣𝑢)
581, 57syl6sseq 3643 . . . . . . 7 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → 𝑘𝐴 𝐵 ⊆ (𝑣𝑢))
5925, 27, 28, 30, 33, 32, 2, 56, 58, 53iunconnlem 21211 . . . . . 6 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → ¬ 𝑃𝑣)
60 ioran 511 . . . . . 6 (¬ (𝑃𝑢𝑃𝑣) ↔ (¬ 𝑃𝑢 ∧ ¬ 𝑃𝑣))
6154, 59, 60sylanbrc 697 . . . . 5 ((((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) ∧ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)) → ¬ (𝑃𝑢𝑃𝑣))
6223, 61pm2.65da 599 . . . 4 (((𝜑 ∧ (𝑢𝐽𝑣𝐽)) ∧ ((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵))) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))
6362ex 450 . . 3 ((𝜑 ∧ (𝑢𝐽𝑣𝐽)) → (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))
6463ralrimivva 2968 . 2 (𝜑 → ∀𝑢𝐽𝑣𝐽 (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣)))
6526ralrimiva 2963 . . . 4 (𝜑 → ∀𝑘𝐴 𝐵𝑋)
66 iunss 4552 . . . 4 ( 𝑘𝐴 𝐵𝑋 ↔ ∀𝑘𝐴 𝐵𝑋)
6765, 66sylibr 224 . . 3 (𝜑 𝑘𝐴 𝐵𝑋)
68 connsub 21205 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑘𝐴 𝐵𝑋) → ((𝐽t 𝑘𝐴 𝐵) ∈ Conn ↔ ∀𝑢𝐽𝑣𝐽 (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))))
6924, 67, 68syl2anc 692 . 2 (𝜑 → ((𝐽t 𝑘𝐴 𝐵) ∈ Conn ↔ ∀𝑢𝐽𝑣𝐽 (((𝑢 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴 𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴 𝐵)) → ¬ 𝑘𝐴 𝐵 ⊆ (𝑢𝑣))))
7064, 69mpbird 247 1 (𝜑 → (𝐽t 𝑘𝐴 𝐵) ∈ Conn)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1036  ∃wex 1702   ∈ wcel 1988   ≠ wne 2791  ∀wral 2909  ∃wrex 2910   ∖ cdif 3564   ∪ cun 3565   ∩ cin 3566   ⊆ wss 3567  ∅c0 3907  ∪ ciun 4511  ‘cfv 5876  (class class class)co 6635   ↾t crest 16062  TopOnctopon 20696  Conncconn 21195 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-oadd 7549  df-er 7727  df-en 7941  df-fin 7944  df-fi 8302  df-rest 16064  df-topgen 16085  df-top 20680  df-topon 20697  df-bases 20731  df-cld 20804  df-conn 21196 This theorem is referenced by:  unconn  21213  conncompconn  21216
 Copyright terms: Public domain W3C validator