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 22704

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 22381	. 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
3		txtop 22628	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×_t 𝐽) ∈ Top)
4	3	anidms 566	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ×_t 𝐽) ∈ Top)
5		idssxp 5945	. . . . . 6 ⊢ ( I ↾ 𝑋) ⊆ (𝑋 × 𝑋)
6	1, 1	txuni 22651	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
7	6	anidms 566	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
8	5, 7	sseqtrid 3969	. . . . 5 ⊢ (𝐽 ∈ Top → ( I ↾ 𝑋) ⊆ ∪ (𝐽 ×_t 𝐽))
9		eqid 2738	. . . . . 6 ⊢ ∪ (𝐽 ×_t 𝐽) = ∪ (𝐽 ×_t 𝐽)
10	9	iscld2 22087	. . . . 5 ⊢ (((𝐽 ×_t 𝐽) ∈ Top ∧ ( I ↾ 𝑋) ⊆ ∪ (𝐽 ×_t 𝐽)) → (( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽)) ↔ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽)))
11	4, 8, 10	syl2anc 583	. . . 4 ⊢ (𝐽 ∈ Top → (( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽)) ↔ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽)))
12		eltx 22627	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → ((∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽) ↔ ∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
13	12	anidms 566	. . . 4 ⊢ (𝐽 ∈ Top → ((∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽) ↔ ∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
14		eldif 3893	. . . . . . . . . 10 ⊢ (𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)))
15	7	eqcomd 2744	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ∪ (𝐽 ×_t 𝐽) = (𝑋 × 𝑋))
16	15	eleq2d 2824	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → (𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ↔ 𝑒 ∈ (𝑋 × 𝑋)))
17	16	anbi1d 629	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) ↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋))))
18	14, 17	syl5bb 282	. . . . . . . . 9 ⊢ (𝐽 ∈ Top → (𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋))))
19	18	imbi1d 341	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
20		impexp 450	. . . . . . . 8 ⊢ (((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
21	19, 20	bitrdi 286	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))))
22	21	ralbidv2 3118	. . . . . 6 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
23		eleq1 2826	. . . . . . . . 9 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ ( I ↾ 𝑋) ↔ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋)))
24	23	notbid 317	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (¬ 𝑒 ∈ ( I ↾ 𝑋) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋)))
25		eleq1 2826	. . . . . . . . . 10 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑)))
26	25	anbi1d 629	. . . . . . . . 9 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
27	26	2rexbidv 3228	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
28	24, 27	imbi12d 344	. . . . . . 7 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
29	28	ralxp 5739	. . . . . 6 ⊢ (∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
30	22, 29	bitrdi 286	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
31		vex 3426	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
32	31	opelresi 5888	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ))
33		ibar 528	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑋 → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )))
34	33	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )))
35		df-br 5071	. . . . . . . . . . . 12 ⊢ (𝑎 I 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ I )
36	31	ideq 5750	. . . . . . . . . . . 12 ⊢ (𝑎 I 𝑏 ↔ 𝑎 = 𝑏)
37	35, 36	bitr3i 276	. . . . . . . . . . 11 ⊢ (⟨𝑎, 𝑏⟩ ∈ I ↔ 𝑎 = 𝑏)
38	34, 37	bitr3di 285	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ) ↔ 𝑎 = 𝑏))
39	32, 38	syl5bb 282	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏))
40	39	adantl 481	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏))
41	40	necon3bbid 2980	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 ≠ 𝑏))
42		elssuni 4868	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ 𝐽 → 𝑐 ⊆ ∪ 𝐽)
43		elssuni 4868	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝐽 → 𝑑 ⊆ ∪ 𝐽)
44		xpss12 5595	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ⊆ ∪ 𝐽 ∧ 𝑑 ⊆ ∪ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽))
45	42, 43, 44	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽))
46	1, 1	xpeq12i 5608	. . . . . . . . . . . . . . 15 ⊢ (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽)
47	45, 46	sseqtrrdi 3968	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋))
48	47	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋))
49	7	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
50	48, 49	sseqtrd 3957	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ ∪ (𝐽 ×_t 𝐽))
51		reldisj 4382	. . . . . . . . . . . 12 ⊢ ((𝑐 × 𝑑) ⊆ ∪ (𝐽 ×_t 𝐽) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
52	50, 51	syl 17	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
53		df-res 5592	. . . . . . . . . . . . . . 15 ⊢ ( I ↾ 𝑋) = ( I ∩ (𝑋 × V))
54	53	ineq2i 4140	. . . . . . . . . . . . . 14 ⊢ ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V)))
55		inass 4150	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V)))
56		inss1 4159	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑐 × 𝑑)
57	56, 48	sstrid 3928	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × 𝑋))
58		ssv 3941	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑋 ⊆ V
59		xpss2 5600	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ⊆ V → (𝑋 × 𝑋) ⊆ (𝑋 × V))
60	58, 59	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 × 𝑋) ⊆ (𝑋 × V)
61	57, 60	sstrdi 3929	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V))
62		df-ss 3900	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V) ↔ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I ))
63	61, 62	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I ))
64	55, 63	eqtr3id 2793	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) = ((𝑐 × 𝑑) ∩ I ))
65	54, 64	eqtrid 2790	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ I ))
66	65	eqeq1d 2740	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ ((𝑐 × 𝑑) ∩ I ) = ∅))
67		opelxp 5616	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑))
68		df-br 5071	. . . . . . . . . . . . . . . 16 ⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ ⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑))
69		elin 3899	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (𝑐 ∩ 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑))
70	67, 68, 69	3bitr4i 302	. . . . . . . . . . . . . . 15 ⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ 𝑎 ∈ (𝑐 ∩ 𝑑))
71	70	notbii 319	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑎(𝑐 × 𝑑)𝑎 ↔ ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
72	71	albii 1823	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎 ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
73		intirr 6012	. . . . . . . . . . . . 13 ⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ ∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎)
74		eq0 4274	. . . . . . . . . . . . 13 ⊢ ((𝑐 ∩ 𝑑) = ∅ ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
75	72, 73, 74	3bitr4i 302	. . . . . . . . . . . 12 ⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅)
76	66, 75	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅))
77	52, 76	bitr3d 280	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑐 ∩ 𝑑) = ∅))
78	77	anbi2d 628	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅)))
79		opelxp 5616	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑))
80	79	anbi1i 623	. . . . . . . . 9 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
81		df-3an 1087	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅))
82	78, 80, 81	3bitr4g 313	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))
83	82	2rexbidva 3227	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))
84	41, 83	imbi12d 344	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
85	84	2ralbidva 3121	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
86	30, 85	bitrd 278	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
87	11, 13, 86	3bitrrd 305	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)) ↔ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))
88	87	pm5.32i 574	. 2 ⊢ ((𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))) ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))
89	2, 88	bitri 274	1 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 ∀wal 1537 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 Vcvv 3422 ∖ cdif 3880 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 ⟨cop 4564 ∪ cuni 4836 class class class wbr 5070 I cid 5479 × cxp 5578 ↾ cres 5582 ‘cfv 6418 (class class class)co 7255 Topctop 21950 Clsdccld 22075 Hauscha 22367 ×_t ctx 22619

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-fv 6426 df-ov 7258 df-oprab 7259 df-mpo 7260 df-1st 7804 df-2nd 7805 df-topgen 17071 df-top 21951 df-topon 21968 df-bases 22004 df-cld 22078 df-haus 22374 df-tx 22621

This theorem is referenced by: hauseqlcld 22705 tgphaus 23176 qtophaus 31688

W3C validator