hausdiag - Metamath Proof Explorer

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

Theorem hausdiag 23149

Description: A topology is Hausdorff iff the diagonal set is closed in the topology's product with itself. EDITORIAL: very clumsy proof, can probably be shortened substantially. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)

**Hypothesis**
Ref	Expression
hausdiag.x	⊢ 𝑋 = ∪ 𝐽

**Assertion**
Ref	Expression
hausdiag	⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))

Proof of Theorem hausdiag Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hausdiag.x	. . 3 ⊢ 𝑋 = ∪ 𝐽
2	1	ishaus 22826	. 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
3		txtop 23073	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×_t 𝐽) ∈ Top)
4	3	anidms 568	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ×_t 𝐽) ∈ Top)
5		idssxp 6049	. . . . . 6 ⊢ ( I ↾ 𝑋) ⊆ (𝑋 × 𝑋)
6	1, 1	txuni 23096	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
7	6	anidms 568	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
8	5, 7	sseqtrid 4035	. . . . 5 ⊢ (𝐽 ∈ Top → ( I ↾ 𝑋) ⊆ ∪ (𝐽 ×_t 𝐽))
9		eqid 2733	. . . . . 6 ⊢ ∪ (𝐽 ×_t 𝐽) = ∪ (𝐽 ×_t 𝐽)
10	9	iscld2 22532	. . . . 5 ⊢ (((𝐽 ×_t 𝐽) ∈ Top ∧ ( I ↾ 𝑋) ⊆ ∪ (𝐽 ×_t 𝐽)) → (( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽)) ↔ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽)))
11	4, 8, 10	syl2anc 585	. . . 4 ⊢ (𝐽 ∈ Top → (( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽)) ↔ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽)))
12		eltx 23072	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → ((∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽) ↔ ∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
13	12	anidms 568	. . . 4 ⊢ (𝐽 ∈ Top → ((∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽) ↔ ∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
14		eldif 3959	. . . . . . . . . 10 ⊢ (𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)))
15	7	eqcomd 2739	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ∪ (𝐽 ×_t 𝐽) = (𝑋 × 𝑋))
16	15	eleq2d 2820	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → (𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ↔ 𝑒 ∈ (𝑋 × 𝑋)))
17	16	anbi1d 631	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) ↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋))))
18	14, 17	bitrid 283	. . . . . . . . 9 ⊢ (𝐽 ∈ Top → (𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋))))
19	18	imbi1d 342	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
20		impexp 452	. . . . . . . 8 ⊢ (((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
21	19, 20	bitrdi 287	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))))
22	21	ralbidv2 3174	. . . . . 6 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
23		eleq1 2822	. . . . . . . . 9 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ ( I ↾ 𝑋) ↔ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋)))
24	23	notbid 318	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (¬ 𝑒 ∈ ( I ↾ 𝑋) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋)))
25		eleq1 2822	. . . . . . . . . 10 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑)))
26	25	anbi1d 631	. . . . . . . . 9 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
27	26	2rexbidv 3220	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
28	24, 27	imbi12d 345	. . . . . . 7 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
29	28	ralxp 5842	. . . . . 6 ⊢ (∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
30	22, 29	bitrdi 287	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
31		vex 3479	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
32	31	opelresi 5990	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ))
33		ibar 530	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑋 → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )))
34	33	adantr 482	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )))
35		df-br 5150	. . . . . . . . . . . 12 ⊢ (𝑎 I 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ I )
36	31	ideq 5853	. . . . . . . . . . . 12 ⊢ (𝑎 I 𝑏 ↔ 𝑎 = 𝑏)
37	35, 36	bitr3i 277	. . . . . . . . . . 11 ⊢ (⟨𝑎, 𝑏⟩ ∈ I ↔ 𝑎 = 𝑏)
38	34, 37	bitr3di 286	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ) ↔ 𝑎 = 𝑏))
39	32, 38	bitrid 283	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏))
40	39	adantl 483	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏))
41	40	necon3bbid 2979	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 ≠ 𝑏))
42		elssuni 4942	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ 𝐽 → 𝑐 ⊆ ∪ 𝐽)
43		elssuni 4942	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝐽 → 𝑑 ⊆ ∪ 𝐽)
44		xpss12 5692	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ⊆ ∪ 𝐽 ∧ 𝑑 ⊆ ∪ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽))
45	42, 43, 44	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽))
46	1, 1	xpeq12i 5705	. . . . . . . . . . . . . . 15 ⊢ (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽)
47	45, 46	sseqtrrdi 4034	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋))
48	47	adantl 483	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋))
49	7	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
50	48, 49	sseqtrd 4023	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ ∪ (𝐽 ×_t 𝐽))
51		reldisj 4452	. . . . . . . . . . . 12 ⊢ ((𝑐 × 𝑑) ⊆ ∪ (𝐽 ×_t 𝐽) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
52	50, 51	syl 17	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
53		df-res 5689	. . . . . . . . . . . . . . 15 ⊢ ( I ↾ 𝑋) = ( I ∩ (𝑋 × V))
54	53	ineq2i 4210	. . . . . . . . . . . . . 14 ⊢ ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V)))
55		inass 4220	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V)))
56		inss1 4229	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑐 × 𝑑)
57	56, 48	sstrid 3994	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × 𝑋))
58		ssv 4007	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑋 ⊆ V
59		xpss2 5697	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ⊆ V → (𝑋 × 𝑋) ⊆ (𝑋 × V))
60	58, 59	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 × 𝑋) ⊆ (𝑋 × V)
61	57, 60	sstrdi 3995	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V))
62		df-ss 3966	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V) ↔ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I ))
63	61, 62	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I ))
64	55, 63	eqtr3id 2787	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) = ((𝑐 × 𝑑) ∩ I ))
65	54, 64	eqtrid 2785	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ I ))
66	65	eqeq1d 2735	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ ((𝑐 × 𝑑) ∩ I ) = ∅))
67		opelxp 5713	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑))
68		df-br 5150	. . . . . . . . . . . . . . . 16 ⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ ⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑))
69		elin 3965	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (𝑐 ∩ 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑))
70	67, 68, 69	3bitr4i 303	. . . . . . . . . . . . . . 15 ⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ 𝑎 ∈ (𝑐 ∩ 𝑑))
71	70	notbii 320	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑎(𝑐 × 𝑑)𝑎 ↔ ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
72	71	albii 1822	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎 ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
73		intirr 6120	. . . . . . . . . . . . 13 ⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ ∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎)
74		eq0 4344	. . . . . . . . . . . . 13 ⊢ ((𝑐 ∩ 𝑑) = ∅ ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
75	72, 73, 74	3bitr4i 303	. . . . . . . . . . . 12 ⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅)
76	66, 75	bitrdi 287	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅))
77	52, 76	bitr3d 281	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑐 ∩ 𝑑) = ∅))
78	77	anbi2d 630	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅)))
79		opelxp 5713	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑))
80	79	anbi1i 625	. . . . . . . . 9 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
81		df-3an 1090	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅))
82	78, 80, 81	3bitr4g 314	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))
83	82	2rexbidva 3218	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))
84	41, 83	imbi12d 345	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
85	84	2ralbidva 3217	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
86	30, 85	bitrd 279	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
87	11, 13, 86	3bitrrd 306	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)) ↔ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))
88	87	pm5.32i 576	. 2 ⊢ ((𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))) ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))
89	2, 88	bitri 275	1 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 ∀wal 1540 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ∖ cdif 3946 ∩ cin 3948 ⊆ wss 3949 ∅c0 4323 ⟨cop 4635 ∪ cuni 4909 class class class wbr 5149 I cid 5574 × cxp 5675 ↾ cres 5679 ‘cfv 6544 (class class class)co 7409 Topctop 22395 Clsdccld 22520 Hauscha 22812 ×_t ctx 23064

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-fv 6552 df-ov 7412 df-oprab 7413 df-mpo 7414 df-1st 7975 df-2nd 7976 df-topgen 17389 df-top 22396 df-topon 22413 df-bases 22449 df-cld 22523 df-haus 22819 df-tx 23066

This theorem is referenced by: hauseqlcld 23150 tgphaus 23621 qtophaus 32816

W3C validator