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

Theorem clssubg 22717
Description: The closure of a subgroup in a topological group is a subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.)
Hypothesis
Ref Expression
subgntr.h 𝐽 = (TopOpen‘𝐺)
Assertion
Ref Expression
clssubg ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ∈ (SubGrp‘𝐺))

Proof of Theorem clssubg
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 subgntr.h . . . . . . 7 𝐽 = (TopOpen‘𝐺)
2 eqid 2801 . . . . . . 7 (Base‘𝐺) = (Base‘𝐺)
31, 2tgptopon 22690 . . . . . 6 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
43adantr 484 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐽 ∈ (TopOn‘(Base‘𝐺)))
5 topontop 21521 . . . . 5 (𝐽 ∈ (TopOn‘(Base‘𝐺)) → 𝐽 ∈ Top)
64, 5syl 17 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐽 ∈ Top)
72subgss 18275 . . . . . 6 (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺))
87adantl 485 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (Base‘𝐺))
9 toponuni 21522 . . . . . 6 (𝐽 ∈ (TopOn‘(Base‘𝐺)) → (Base‘𝐺) = 𝐽)
104, 9syl 17 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (Base‘𝐺) = 𝐽)
118, 10sseqtrd 3958 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 𝐽)
12 eqid 2801 . . . . 5 𝐽 = 𝐽
1312clsss3 21667 . . . 4 ((𝐽 ∈ Top ∧ 𝑆 𝐽) → ((cls‘𝐽)‘𝑆) ⊆ 𝐽)
146, 11, 13syl2anc 587 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ⊆ 𝐽)
1514, 10sseqtrrd 3959 . 2 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ⊆ (Base‘𝐺))
1612sscls 21664 . . . 4 ((𝐽 ∈ Top ∧ 𝑆 𝐽) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
176, 11, 16syl2anc 587 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
18 eqid 2801 . . . . . 6 (0g𝐺) = (0g𝐺)
1918subg0cl 18282 . . . . 5 (𝑆 ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ 𝑆)
2019adantl 485 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (0g𝐺) ∈ 𝑆)
2120ne0d 4254 . . 3 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ≠ ∅)
22 ssn0 4311 . . 3 ((𝑆 ⊆ ((cls‘𝐽)‘𝑆) ∧ 𝑆 ≠ ∅) → ((cls‘𝐽)‘𝑆) ≠ ∅)
2317, 21, 22syl2anc 587 . 2 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ≠ ∅)
24 df-ov 7142 . . . 4 (𝑥(-g𝐺)𝑦) = ((-g𝐺)‘⟨𝑥, 𝑦⟩)
25 opelxpi 5560 . . . . . . 7 ((𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆)) → ⟨𝑥, 𝑦⟩ ∈ (((cls‘𝐽)‘𝑆) × ((cls‘𝐽)‘𝑆)))
26 txcls 22212 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘(Base‘𝐺)) ∧ 𝐽 ∈ (TopOn‘(Base‘𝐺))) ∧ (𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ⊆ (Base‘𝐺))) → ((cls‘(𝐽 ×t 𝐽))‘(𝑆 × 𝑆)) = (((cls‘𝐽)‘𝑆) × ((cls‘𝐽)‘𝑆)))
274, 4, 8, 8, 26syl22anc 837 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘(𝐽 ×t 𝐽))‘(𝑆 × 𝑆)) = (((cls‘𝐽)‘𝑆) × ((cls‘𝐽)‘𝑆)))
28 txtopon 22199 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘(Base‘𝐺)) ∧ 𝐽 ∈ (TopOn‘(Base‘𝐺))) → (𝐽 ×t 𝐽) ∈ (TopOn‘((Base‘𝐺) × (Base‘𝐺))))
294, 4, 28syl2anc 587 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝐽 ×t 𝐽) ∈ (TopOn‘((Base‘𝐺) × (Base‘𝐺))))
30 topontop 21521 . . . . . . . . . . . 12 ((𝐽 ×t 𝐽) ∈ (TopOn‘((Base‘𝐺) × (Base‘𝐺))) → (𝐽 ×t 𝐽) ∈ Top)
3129, 30syl 17 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝐽 ×t 𝐽) ∈ Top)
32 cnvimass 5920 . . . . . . . . . . . . 13 ((-g𝐺) “ 𝑆) ⊆ dom (-g𝐺)
33 tgpgrp 22686 . . . . . . . . . . . . . . 15 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
3433adantr 484 . . . . . . . . . . . . . 14 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐺 ∈ Grp)
35 eqid 2801 . . . . . . . . . . . . . . 15 (-g𝐺) = (-g𝐺)
362, 35grpsubf 18173 . . . . . . . . . . . . . 14 (𝐺 ∈ Grp → (-g𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
3734, 36syl 17 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (-g𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺))
3832, 37fssdm 6508 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((-g𝐺) “ 𝑆) ⊆ ((Base‘𝐺) × (Base‘𝐺)))
39 toponuni 21522 . . . . . . . . . . . . 13 ((𝐽 ×t 𝐽) ∈ (TopOn‘((Base‘𝐺) × (Base‘𝐺))) → ((Base‘𝐺) × (Base‘𝐺)) = (𝐽 ×t 𝐽))
4029, 39syl 17 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((Base‘𝐺) × (Base‘𝐺)) = (𝐽 ×t 𝐽))
4138, 40sseqtrd 3958 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((-g𝐺) “ 𝑆) ⊆ (𝐽 ×t 𝐽))
4235subgsubcl 18285 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥𝑆𝑦𝑆) → (𝑥(-g𝐺)𝑦) ∈ 𝑆)
43423expb 1117 . . . . . . . . . . . . . . 15 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥(-g𝐺)𝑦) ∈ 𝑆)
4443ralrimivva 3159 . . . . . . . . . . . . . 14 (𝑆 ∈ (SubGrp‘𝐺) → ∀𝑥𝑆𝑦𝑆 (𝑥(-g𝐺)𝑦) ∈ 𝑆)
45 fveq2 6649 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → ((-g𝐺)‘𝑧) = ((-g𝐺)‘⟨𝑥, 𝑦⟩))
4645, 24eqtr4di 2854 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → ((-g𝐺)‘𝑧) = (𝑥(-g𝐺)𝑦))
4746eleq1d 2877 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → (((-g𝐺)‘𝑧) ∈ 𝑆 ↔ (𝑥(-g𝐺)𝑦) ∈ 𝑆))
4847ralxp 5680 . . . . . . . . . . . . . 14 (∀𝑧 ∈ (𝑆 × 𝑆)((-g𝐺)‘𝑧) ∈ 𝑆 ↔ ∀𝑥𝑆𝑦𝑆 (𝑥(-g𝐺)𝑦) ∈ 𝑆)
4944, 48sylibr 237 . . . . . . . . . . . . 13 (𝑆 ∈ (SubGrp‘𝐺) → ∀𝑧 ∈ (𝑆 × 𝑆)((-g𝐺)‘𝑧) ∈ 𝑆)
5049adantl 485 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ∀𝑧 ∈ (𝑆 × 𝑆)((-g𝐺)‘𝑧) ∈ 𝑆)
5137ffund 6495 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → Fun (-g𝐺))
52 xpss12 5538 . . . . . . . . . . . . . . 15 ((𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑆 × 𝑆) ⊆ ((Base‘𝐺) × (Base‘𝐺)))
538, 8, 52syl2anc 587 . . . . . . . . . . . . . 14 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑆 × 𝑆) ⊆ ((Base‘𝐺) × (Base‘𝐺)))
5437fdmd 6501 . . . . . . . . . . . . . 14 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → dom (-g𝐺) = ((Base‘𝐺) × (Base‘𝐺)))
5553, 54sseqtrrd 3959 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑆 × 𝑆) ⊆ dom (-g𝐺))
56 funimass5 6806 . . . . . . . . . . . . 13 ((Fun (-g𝐺) ∧ (𝑆 × 𝑆) ⊆ dom (-g𝐺)) → ((𝑆 × 𝑆) ⊆ ((-g𝐺) “ 𝑆) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)((-g𝐺)‘𝑧) ∈ 𝑆))
5751, 55, 56syl2anc 587 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((𝑆 × 𝑆) ⊆ ((-g𝐺) “ 𝑆) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)((-g𝐺)‘𝑧) ∈ 𝑆))
5850, 57mpbird 260 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑆 × 𝑆) ⊆ ((-g𝐺) “ 𝑆))
59 eqid 2801 . . . . . . . . . . . 12 (𝐽 ×t 𝐽) = (𝐽 ×t 𝐽)
6059clsss 21662 . . . . . . . . . . 11 (((𝐽 ×t 𝐽) ∈ Top ∧ ((-g𝐺) “ 𝑆) ⊆ (𝐽 ×t 𝐽) ∧ (𝑆 × 𝑆) ⊆ ((-g𝐺) “ 𝑆)) → ((cls‘(𝐽 ×t 𝐽))‘(𝑆 × 𝑆)) ⊆ ((cls‘(𝐽 ×t 𝐽))‘((-g𝐺) “ 𝑆)))
6131, 41, 58, 60syl3anc 1368 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘(𝐽 ×t 𝐽))‘(𝑆 × 𝑆)) ⊆ ((cls‘(𝐽 ×t 𝐽))‘((-g𝐺) “ 𝑆)))
621, 35tgpsubcn 22698 . . . . . . . . . . . 12 (𝐺 ∈ TopGrp → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
6362adantr 484 . . . . . . . . . . 11 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
6412cncls2i 21878 . . . . . . . . . . 11 (((-g𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ 𝑆 𝐽) → ((cls‘(𝐽 ×t 𝐽))‘((-g𝐺) “ 𝑆)) ⊆ ((-g𝐺) “ ((cls‘𝐽)‘𝑆)))
6563, 11, 64syl2anc 587 . . . . . . . . . 10 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘(𝐽 ×t 𝐽))‘((-g𝐺) “ 𝑆)) ⊆ ((-g𝐺) “ ((cls‘𝐽)‘𝑆)))
6661, 65sstrd 3928 . . . . . . . . 9 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘(𝐽 ×t 𝐽))‘(𝑆 × 𝑆)) ⊆ ((-g𝐺) “ ((cls‘𝐽)‘𝑆)))
6727, 66eqsstrrd 3957 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (((cls‘𝐽)‘𝑆) × ((cls‘𝐽)‘𝑆)) ⊆ ((-g𝐺) “ ((cls‘𝐽)‘𝑆)))
6867sselda 3918 . . . . . . 7 (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ ⟨𝑥, 𝑦⟩ ∈ (((cls‘𝐽)‘𝑆) × ((cls‘𝐽)‘𝑆))) → ⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ ((cls‘𝐽)‘𝑆)))
6925, 68sylan2 595 . . . . . 6 (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → ⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ ((cls‘𝐽)‘𝑆)))
7033ad2antrr 725 . . . . . . 7 (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → 𝐺 ∈ Grp)
71 ffn 6491 . . . . . . 7 ((-g𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → (-g𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)))
72 elpreima 6809 . . . . . . 7 ((-g𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ ((cls‘𝐽)‘𝑆)) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ ((cls‘𝐽)‘𝑆))))
7370, 36, 71, 724syl 19 . . . . . 6 (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → (⟨𝑥, 𝑦⟩ ∈ ((-g𝐺) “ ((cls‘𝐽)‘𝑆)) ↔ (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ ((cls‘𝐽)‘𝑆))))
7469, 73mpbid 235 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → (⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ ((cls‘𝐽)‘𝑆)))
7574simprd 499 . . . 4 (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → ((-g𝐺)‘⟨𝑥, 𝑦⟩) ∈ ((cls‘𝐽)‘𝑆))
7624, 75eqeltrid 2897 . . 3 (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → (𝑥(-g𝐺)𝑦) ∈ ((cls‘𝐽)‘𝑆))
7776ralrimivva 3159 . 2 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ∀𝑥 ∈ ((cls‘𝐽)‘𝑆)∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(-g𝐺)𝑦) ∈ ((cls‘𝐽)‘𝑆))
782, 35issubg4 18293 . . 3 (𝐺 ∈ Grp → (((cls‘𝐽)‘𝑆) ∈ (SubGrp‘𝐺) ↔ (((cls‘𝐽)‘𝑆) ⊆ (Base‘𝐺) ∧ ((cls‘𝐽)‘𝑆) ≠ ∅ ∧ ∀𝑥 ∈ ((cls‘𝐽)‘𝑆)∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(-g𝐺)𝑦) ∈ ((cls‘𝐽)‘𝑆))))
7934, 78syl 17 . 2 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (((cls‘𝐽)‘𝑆) ∈ (SubGrp‘𝐺) ↔ (((cls‘𝐽)‘𝑆) ⊆ (Base‘𝐺) ∧ ((cls‘𝐽)‘𝑆) ≠ ∅ ∧ ∀𝑥 ∈ ((cls‘𝐽)‘𝑆)∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(-g𝐺)𝑦) ∈ ((cls‘𝐽)‘𝑆))))
8015, 23, 77, 79mpbir3and 1339 1 ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ∈ (SubGrp‘𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  wne 2990  wral 3109  wss 3884  c0 4246  cop 4534   cuni 4803   × cxp 5521  ccnv 5522  dom cdm 5523  cima 5526  Fun wfun 6322   Fn wfn 6323  wf 6324  cfv 6328  (class class class)co 7139  Basecbs 16478  TopOpenctopn 16690  0gc0g 16708  Grpcgrp 18098  -gcsg 18100  SubGrpcsubg 18268  Topctop 21501  TopOnctopon 21518  clsccl 21626   Cn ccn 21832   ×t ctx 22168  TopGrpctgp 22679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-2 11692  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-0g 16710  df-topgen 16712  df-plusf 17846  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-grp 18101  df-minusg 18102  df-sbg 18103  df-subg 18271  df-top 21502  df-topon 21519  df-topsp 21541  df-bases 21554  df-cld 21627  df-ntr 21628  df-cls 21629  df-cn 21835  df-tx 22170  df-tmd 22680  df-tgp 22681
This theorem is referenced by:  clsnsg  22718  tgptsmscls  22758
  Copyright terms: Public domain W3C validator