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 23964

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 23640	. 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
3		txtop 23888	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×_t 𝐽) ∈ Top)
4	3	anidms 577	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ×_t 𝐽) ∈ Top)
5		idssxp 6041	. . . . . 6 ⊢ ( I ↾ 𝑋) ⊆ (𝑋 × 𝑋)
6	1, 1	txuni 23911	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
7	6	anidms 577	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
8	5, 7	sseqtrid 3973	. . . . 5 ⊢ (𝐽 ∈ Top → ( I ↾ 𝑋) ⊆ ∪ (𝐽 ×_t 𝐽))
9		eqid 2761	. . . . . 6 ⊢ ∪ (𝐽 ×_t 𝐽) = ∪ (𝐽 ×_t 𝐽)
10	9	iscld2 23346	. . . . 5 ⊢ (((𝐽 ×_t 𝐽) ∈ Top ∧ ( I ↾ 𝑋) ⊆ ∪ (𝐽 ×_t 𝐽)) → (( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽)) ↔ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽)))
11	4, 8, 10	syl2anc 596	. . . 4 ⊢ (𝐽 ∈ Top → (( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽)) ↔ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽)))
12		eltx 23887	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → ((∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽) ↔ ∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
13	12	anidms 577	. . . 4 ⊢ (𝐽 ∈ Top → ((∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽) ↔ ∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
14		eldif 3909	. . . . . . . . . 10 ⊢ (𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)))
15	7	eqcomd 2767	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ∪ (𝐽 ×_t 𝐽) = (𝑋 × 𝑋))
16	15	eleq2d 2847	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → (𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ↔ 𝑒 ∈ (𝑋 × 𝑋)))
17	16	anbi1d 643	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) ↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋))))
18	14, 17	bitrid 286	. . . . . . . . 9 ⊢ (𝐽 ∈ Top → (𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋))))
19	18	imbi1d 344	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
20		impexp 456	. . . . . . . 8 ⊢ (((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
21	19, 20	bitrdi 290	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))))
22	21	ralbidv2 3182	. . . . . 6 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
23		eleq1 2849	. . . . . . . . 9 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ ( I ↾ 𝑋) ↔ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋)))
24	23	notbid 321	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (¬ 𝑒 ∈ ( I ↾ 𝑋) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋)))
25		eleq1 2849	. . . . . . . . . 10 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑)))
26	25	anbi1d 643	. . . . . . . . 9 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
27	26	2rexbidv 3228	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
28	24, 27	imbi12d 347	. . . . . . 7 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
29	28	ralxp 5818	. . . . . 6 ⊢ (∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
30	22, 29	bitrdi 290	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
31		vex 3455	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
32	31	opelresi 5978	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ))
33		ibar 538	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑋 → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )))
34	33	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )))
35		df-br 5104	. . . . . . . . . . . 12 ⊢ (𝑎 I 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ I )
36	31	ideq 5830	. . . . . . . . . . . 12 ⊢ (𝑎 I 𝑏 ↔ 𝑎 = 𝑏)
37	35, 36	bitr3i 280	. . . . . . . . . . 11 ⊢ (⟨𝑎, 𝑏⟩ ∈ I ↔ 𝑎 = 𝑏)
38	34, 37	bitr3di 289	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ) ↔ 𝑎 = 𝑏))
39	32, 38	bitrid 286	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏))
40	39	adantl 487	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏))
41	40	necon3bbid 2993	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 ≠ 𝑏))
42		elssuni 4899	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ 𝐽 → 𝑐 ⊆ ∪ 𝐽)
43		elssuni 4899	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝐽 → 𝑑 ⊆ ∪ 𝐽)
44		xpss12 5666	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ⊆ ∪ 𝐽 ∧ 𝑑 ⊆ ∪ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽))
45	42, 43, 44	syl2an 608	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽))
46	1, 1	xpeq12i 5679	. . . . . . . . . . . . . . 15 ⊢ (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽)
47	45, 46	sseqtrrdi 3972	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋))
48	47	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋))
49	7	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
50	48, 49	sseqtrd 3967	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ ∪ (𝐽 ×_t 𝐽))
51		reldisj 4406	. . . . . . . . . . . 12 ⊢ ((𝑐 × 𝑑) ⊆ ∪ (𝐽 ×_t 𝐽) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
52	50, 51	syl 18	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
53		df-res 5663	. . . . . . . . . . . . . . 15 ⊢ ( I ↾ 𝑋) = ( I ∩ (𝑋 × V))
54	53	ineq2i 4163	. . . . . . . . . . . . . 14 ⊢ ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V)))
55		inass 4173	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V)))
56		inss1 4182	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑐 × 𝑑)
57	56, 48	sstrid 3942	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × 𝑋))
58		ssv 3955	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑋 ⊆ V
59		xpss2 5671	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ⊆ V → (𝑋 × 𝑋) ⊆ (𝑋 × V))
60	58, 59	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 × 𝑋) ⊆ (𝑋 × V)
61	57, 60	sstrdi 3943	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V))
62		dfss2 3917	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V) ↔ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I ))
63	61, 62	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I ))
64	55, 63	eqtr3id 2810	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) = ((𝑐 × 𝑑) ∩ I ))
65	54, 64	eqtrid 2808	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ I ))
66	65	eqeq1d 2763	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ ((𝑐 × 𝑑) ∩ I ) = ∅))
67		opelxp 5687	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑))
68		df-br 5104	. . . . . . . . . . . . . . . 16 ⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ ⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑))
69		elin 3915	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (𝑐 ∩ 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑))
70	67, 68, 69	3bitr4i 306	. . . . . . . . . . . . . . 15 ⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ 𝑎 ∈ (𝑐 ∩ 𝑑))
71	70	notbii 323	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑎(𝑐 × 𝑑)𝑎 ↔ ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
72	71	albii 1852	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎 ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
73		intirr 6112	. . . . . . . . . . . . 13 ⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ ∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎)
74		eq0 4297	. . . . . . . . . . . . 13 ⊢ ((𝑐 ∩ 𝑑) = ∅ ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
75	72, 73, 74	3bitr4i 306	. . . . . . . . . . . 12 ⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅)
76	66, 75	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅))
77	52, 76	bitr3d 284	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑐 ∩ 𝑑) = ∅))
78	77	anbi2d 642	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅)))
79		opelxp 5687	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑))
80	79	anbi1i 636	. . . . . . . . 9 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
81		df-3an 1105	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅))
82	78, 80, 81	3bitr4g 317	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))
83	82	2rexbidva 3226	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))
84	41, 83	imbi12d 347	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
85	84	2ralbidva 3225	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
86	30, 85	bitrd 282	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
87	11, 13, 86	3bitrrd 309	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)) ↔ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))
88	87	pm5.32i 585	. 2 ⊢ ((𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))) ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))
89	2, 88	bitri 278	1 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 ∀wal 1568 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 Vcvv 3451 ∖ cdif 3896 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 ⟨cop 4590 ∪ cuni 4867 class class class wbr 5103 I cid 5545 × cxp 5649 ↾ cres 5653 ‘cfv 6538 (class class class)co 7420 Topctop 23211 Clsdccld 23334 Hauscha 23626 ×_t ctx 23879

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-fv 6546 df-ov 7423 df-oprab 7424 df-mpo 7425 df-1st 8001 df-2nd 8002 df-topgen 17614 df-top 23212 df-topon 23229 df-bases 23264 df-cld 23337 df-haus 23633 df-tx 23881

This theorem is used by: hauseqlcld 23965 tgphaus 24436 qtophaus 34468

W3C validator