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 22250

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 21927	. 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
3		txtop 22174	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×_t 𝐽) ∈ Top)
4	3	anidms 570	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ×_t 𝐽) ∈ Top)
5		idssxp 5883	. . . . . 6 ⊢ ( I ↾ 𝑋) ⊆ (𝑋 × 𝑋)
6	1, 1	txuni 22197	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
7	6	anidms 570	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
8	5, 7	sseqtrid 3967	. . . . 5 ⊢ (𝐽 ∈ Top → ( I ↾ 𝑋) ⊆ ∪ (𝐽 ×_t 𝐽))
9		eqid 2798	. . . . . 6 ⊢ ∪ (𝐽 ×_t 𝐽) = ∪ (𝐽 ×_t 𝐽)
10	9	iscld2 21633	. . . . 5 ⊢ (((𝐽 ×_t 𝐽) ∈ Top ∧ ( I ↾ 𝑋) ⊆ ∪ (𝐽 ×_t 𝐽)) → (( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽)) ↔ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽)))
11	4, 8, 10	syl2anc 587	. . . 4 ⊢ (𝐽 ∈ Top → (( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽)) ↔ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽)))
12		eltx 22173	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → ((∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽) ↔ ∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
13	12	anidms 570	. . . 4 ⊢ (𝐽 ∈ Top → ((∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽) ↔ ∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
14		eldif 3891	. . . . . . . . . 10 ⊢ (𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)))
15	7	eqcomd 2804	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ∪ (𝐽 ×_t 𝐽) = (𝑋 × 𝑋))
16	15	eleq2d 2875	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → (𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ↔ 𝑒 ∈ (𝑋 × 𝑋)))
17	16	anbi1d 632	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) ↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋))))
18	14, 17	syl5bb 286	. . . . . . . . 9 ⊢ (𝐽 ∈ Top → (𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋))))
19	18	imbi1d 345	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
20		impexp 454	. . . . . . . 8 ⊢ (((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
21	19, 20	syl6bb 290	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))))
22	21	ralbidv2 3160	. . . . . 6 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
23		eleq1 2877	. . . . . . . . 9 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ ( I ↾ 𝑋) ↔ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋)))
24	23	notbid 321	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (¬ 𝑒 ∈ ( I ↾ 𝑋) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋)))
25		eleq1 2877	. . . . . . . . . 10 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑)))
26	25	anbi1d 632	. . . . . . . . 9 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
27	26	2rexbidv 3259	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
28	24, 27	imbi12d 348	. . . . . . 7 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
29	28	ralxp 5676	. . . . . 6 ⊢ (∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
30	22, 29	syl6bb 290	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
31		vex 3444	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
32	31	opelresi 5826	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ))
33		ibar 532	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑋 → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )))
34	33	adantr 484	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )))
35		df-br 5031	. . . . . . . . . . . 12 ⊢ (𝑎 I 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ I )
36	31	ideq 5687	. . . . . . . . . . . 12 ⊢ (𝑎 I 𝑏 ↔ 𝑎 = 𝑏)
37	35, 36	bitr3i 280	. . . . . . . . . . 11 ⊢ (⟨𝑎, 𝑏⟩ ∈ I ↔ 𝑎 = 𝑏)
38	34, 37	bitr3di 289	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ) ↔ 𝑎 = 𝑏))
39	32, 38	syl5bb 286	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏))
40	39	adantl 485	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏))
41	40	necon3bbid 3024	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 ≠ 𝑏))
42		elssuni 4830	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ 𝐽 → 𝑐 ⊆ ∪ 𝐽)
43		elssuni 4830	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝐽 → 𝑑 ⊆ ∪ 𝐽)
44		xpss12 5534	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ⊆ ∪ 𝐽 ∧ 𝑑 ⊆ ∪ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽))
45	42, 43, 44	syl2an 598	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽))
46	1, 1	xpeq12i 5547	. . . . . . . . . . . . . . 15 ⊢ (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽)
47	45, 46	sseqtrrdi 3966	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋))
48	47	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋))
49	7	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
50	48, 49	sseqtrd 3955	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ ∪ (𝐽 ×_t 𝐽))
51		reldisj 4359	. . . . . . . . . . . 12 ⊢ ((𝑐 × 𝑑) ⊆ ∪ (𝐽 ×_t 𝐽) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
52	50, 51	syl 17	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
53		df-res 5531	. . . . . . . . . . . . . . 15 ⊢ ( I ↾ 𝑋) = ( I ∩ (𝑋 × V))
54	53	ineq2i 4136	. . . . . . . . . . . . . 14 ⊢ ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V)))
55		inass 4146	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V)))
56		inss1 4155	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑐 × 𝑑)
57	56, 48	sstrid 3926	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × 𝑋))
58		ssv 3939	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑋 ⊆ V
59		xpss2 5539	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ⊆ V → (𝑋 × 𝑋) ⊆ (𝑋 × V))
60	58, 59	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 × 𝑋) ⊆ (𝑋 × V)
61	57, 60	sstrdi 3927	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V))
62		df-ss 3898	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V) ↔ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I ))
63	61, 62	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I ))
64	55, 63	syl5eqr 2847	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) = ((𝑐 × 𝑑) ∩ I ))
65	54, 64	syl5eq 2845	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ I ))
66	65	eqeq1d 2800	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ ((𝑐 × 𝑑) ∩ I ) = ∅))
67		opelxp 5555	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑))
68		df-br 5031	. . . . . . . . . . . . . . . 16 ⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ ⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑))
69		elin 3897	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (𝑐 ∩ 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑))
70	67, 68, 69	3bitr4i 306	. . . . . . . . . . . . . . 15 ⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ 𝑎 ∈ (𝑐 ∩ 𝑑))
71	70	notbii 323	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑎(𝑐 × 𝑑)𝑎 ↔ ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
72	71	albii 1821	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎 ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
73		intirr 5945	. . . . . . . . . . . . 13 ⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ ∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎)
74		eq0 4258	. . . . . . . . . . . . 13 ⊢ ((𝑐 ∩ 𝑑) = ∅ ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
75	72, 73, 74	3bitr4i 306	. . . . . . . . . . . 12 ⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅)
76	66, 75	syl6bb 290	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 ∩ 𝑑) = ∅))
77	52, 76	bitr3d 284	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑐 ∩ 𝑑) = ∅))
78	77	anbi2d 631	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅)))
79		opelxp 5555	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑))
80	79	anbi1i 626	. . . . . . . . 9 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
81		df-3an 1086	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅))
82	78, 80, 81	3bitr4g 317	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))
83	82	2rexbidva 3258	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))
84	41, 83	imbi12d 348	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
85	84	2ralbidva 3163	. . . . 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 578	. 2 ⊢ ((𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))) ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))
89	2, 88	bitri 278	1 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 ∀wal 1536 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 ∃wrex 3107 Vcvv 3441 ∖ cdif 3878 ∩ cin 3880 ⊆ wss 3881 ∅c0 4243 ⟨cop 4531 ∪ cuni 4800 class class class wbr 5030 I cid 5424 × cxp 5517 ↾ cres 5521 ‘cfv 6324 (class class class)co 7135 Topctop 21498 Clsdccld 21621 Hauscha 21913 ×_t ctx 22165

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 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-1st 7671 df-2nd 7672 df-topgen 16709 df-top 21499 df-topon 21516 df-bases 21551 df-cld 21624 df-haus 21920 df-tx 22167

This theorem is referenced by: hauseqlcld 22251 tgphaus 22722 qtophaus 31189

W3C validator