hausflim - Metamath Proof Explorer

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

Theorem hausflim 23868

Description: A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)

**Hypothesis**
Ref	Expression
flimcf.1	⊢ 𝑋 = ∪ 𝐽

**Assertion**
Ref	Expression
hausflim	⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))

Distinct variable groups: 𝑥,𝑓,𝐽 𝑓,𝑋,𝑥

Proof of Theorem hausflim Dummy variables 𝑣 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		haustop 23218	. . 3 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
2		hausflimi 23867	. . . 4 ⊢ (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
3	2	ralrimivw 3129	. . 3 ⊢ (𝐽 ∈ Haus → ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
4	1, 3	jca 511	. 2 ⊢ (𝐽 ∈ Haus → (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
5		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝐽 ∈ Top)
6		flimcf.1	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = ∪ 𝐽
7	6	toptopon 22804	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
8	5, 7	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝐽 ∈ (TopOn‘𝑋))
9		simprll 778	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑧 ∈ 𝑋)
10	9	snssd 4773	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑧} ⊆ 𝑋)
11	9	snn0d 4739	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑧} ≠ ∅)
12		neifil 23767	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑧} ⊆ 𝑋 ∧ {𝑧} ≠ ∅) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
13	8, 10, 11, 12	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
14		filfbas 23735	. . . . . . . . . . . 12 ⊢ (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
15	13, 14	syl 17	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
16		simprlr 779	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑤 ∈ 𝑋)
17	16	snssd 4773	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑤} ⊆ 𝑋)
18	16	snn0d 4739	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → {𝑤} ≠ ∅)
19		neifil 23767	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑤} ⊆ 𝑋 ∧ {𝑤} ≠ ∅) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
20	8, 17, 18, 19	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
21		filfbas 23735	. . . . . . . . . . . 12 ⊢ (((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
23		fbunfip 23756	. . . . . . . . . . 11 ⊢ ((((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅))
24	15, 22, 23	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅))
25	6	neisspw 22994	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑧}) ⊆ 𝒫 𝑋)
26	6	neisspw 22994	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑤}) ⊆ 𝒫 𝑋)
27	25, 26	unssd 4155	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋)
28	27	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋)
29	28	a1d 25	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋))
30		ssun1 4141	. . . . . . . . . . . . . 14 ⊢ ((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))
31		filn0 23749	. . . . . . . . . . . . . . 15 ⊢ (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
32	13, 31	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
33		ssn0 4367	. . . . . . . . . . . . . 14 ⊢ ((((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∧ ((nei‘𝐽)‘{𝑧}) ≠ ∅) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
34	30, 32, 33	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
35	34	a1d 25	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅))
36		idd 24	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
37	29, 35, 36	3jcad 1129	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
38	6	topopn 22793	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
39	38	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → 𝑋 ∈ 𝐽)
40		fsubbas 23754	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝐽 → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
41	39, 40	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
42		fgcl 23765	. . . . . . . . . . . . . . 15 ⊢ ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋))
43	42	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋))
44		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ≠ 𝑤)
45	9	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ∈ 𝑋)
46	16	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤 ∈ 𝑋)
47		fvex 6871	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((nei‘𝐽)‘{𝑧}) ∈ V
48		fvex 6871	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((nei‘𝐽)‘{𝑤}) ∈ V
49	47, 48	unex 7720	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V
50		ssfii 9370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))
51	49, 50	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))
52		ssfg 23759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
53	52	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
54	51, 53	sstrid 3958	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
55	30, 54	sstrid 3958	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
56	8	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
57		elflim 23858	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
58	56, 43, 57	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
59	45, 55, 58	mpbir2and 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
60	54	unssbd 4157	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
61		elflim 23858	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
62	56, 43, 61	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
63	46, 60, 62	mpbir2and 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
64		eleq1w 2811	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
65		eleq1w 2811	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
66	64, 65	moi 3689	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → 𝑧 = 𝑤)
67	66	3com23 1126	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → 𝑧 = 𝑤)
68	67	3expia 1121	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
69	45, 46, 59, 63, 68	syl22anc 838	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
70	69	necon3ad 2938	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧 ≠ 𝑤 → ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
71	44, 70	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
72		oveq2 7395	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝐽 fLim 𝑓) = (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
73	72	eleq2d 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝑥 ∈ (𝐽 fLim 𝑓) ↔ 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
74	73	mobidv 2542	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ∃𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
75	74	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (¬ ∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
76	75	rspcev 3588	. . . . . . . . . . . . . 14 ⊢ (((𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋) ∧ ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
77	43, 71, 76	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
78	77	ex 412	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
79	41, 78	sylbird 260	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
80	37, 79	syld 47	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
81	24, 80	sylbird 260	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
82		df-ne 2926	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ (𝑢 ∩ 𝑣) = ∅)
83	82	ralbii 3075	. . . . . . . . . . . 12 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢 ∩ 𝑣) = ∅)
84		ralnex 3055	. . . . . . . . . . . 12 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢 ∩ 𝑣) = ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
85	83, 84	bitri 275	. . . . . . . . . . 11 ⊢ (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
86	85	ralbii 3075	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
87		ralnex 3055	. . . . . . . . . 10 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
88	86, 87	bitri 275	. . . . . . . . 9 ⊢ (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) ≠ ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
89		rexnal 3082	. . . . . . . . 9 ⊢ (∃𝑓 ∈ (Fil‘𝑋) ¬ ∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ¬ ∀𝑓 ∈ (Fil‘𝑋)∃𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
90	81, 88, 89	3imtr3g 295	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅ → ¬ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
91	90	con4d 115	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → (∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅))
92	91	imp 406	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
93	92	an32s 652	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑧 ≠ 𝑤)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)
94	93	expr 456	. . . 4 ⊢ (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅))
95	94	ralrimivva 3180	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅))
96		simpl 482	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ Top)
97	96, 7	sylib 218	. . . 4 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ (TopOn‘𝑋))
98		hausnei2 23240	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Haus ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)))
99	97, 98	syl 17	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → (𝐽 ∈ Haus ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (𝑧 ≠ 𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢 ∩ 𝑣) = ∅)))
100	95, 99	mpbird 257	. 2 ⊢ ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ Haus)
101	4, 100	impbii 209	1 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∃*wmo 2531 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 Vcvv 3447 ∪ cun 3912 ∩ cin 3913 ⊆ wss 3914 ∅c0 4296 𝒫 cpw 4563 {csn 4589 ∪ cuni 4871 ‘cfv 6511 (class class class)co 7387 ficfi 9361 fBascfbas 21252 filGencfg 21253 Topctop 22780 TopOnctopon 22797 neicnei 22984 Hauscha 23195 Filcfil 23732 fLim cflim 23821

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1o 8434 df-2o 8435 df-en 8919 df-fin 8922 df-fi 9362 df-fbas 21261 df-fg 21262 df-top 22781 df-topon 22798 df-nei 22985 df-haus 23202 df-fil 23733 df-flim 23826

This theorem is referenced by: (None)

W3C validator