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 23539

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 23216	. 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
3		txtop 23463	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×_t 𝐽) ∈ Top)
4	3	anidms 566	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ×_t 𝐽) ∈ Top)
5		idssxp 6023	. . . . . 6 ⊢ ( I ↾ 𝑋) ⊆ (𝑋 × 𝑋)
6	1, 1	txuni 23486	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
7	6	anidms 566	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
8	5, 7	sseqtrid 3992	. . . . 5 ⊢ (𝐽 ∈ Top → ( I ↾ 𝑋) ⊆ ∪ (𝐽 ×_t 𝐽))
9		eqid 2730	. . . . . 6 ⊢ ∪ (𝐽 ×_t 𝐽) = ∪ (𝐽 ×_t 𝐽)
10	9	iscld2 22922	. . . . 5 ⊢ (((𝐽 ×_t 𝐽) ∈ Top ∧ ( I ↾ 𝑋) ⊆ ∪ (𝐽 ×_t 𝐽)) → (( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽)) ↔ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽)))
11	4, 8, 10	syl2anc 584	. . . 4 ⊢ (𝐽 ∈ Top → (( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×_t 𝐽)) ↔ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ∈ (𝐽 ×_t 𝐽)))
12		eltx 23462	. . . . 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 3927	. . . . . . . . . 10 ⊢ (𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) ↔ (𝑒 ∈ ∪ (𝐽 ×_t 𝐽) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)))
15	7	eqcomd 2736	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ∪ (𝐽 ×_t 𝐽) = (𝑋 × 𝑋))
16	15	eleq2d 2815	. . . . . . . . . . 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 341	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
20		impexp 450	. . . . . . . 8 ⊢ (((𝑒 ∈ (𝑋 × 𝑋) ∧ ¬ 𝑒 ∈ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
21	19, 20	bitrdi 287	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑒 ∈ (𝑋 × 𝑋) → (¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))))
22	21	ralbidv2 3153	. . . . . 6 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
23		eleq1 2817	. . . . . . . . 9 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ ( I ↾ 𝑋) ↔ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋)))
24	23	notbid 318	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (¬ 𝑒 ∈ ( I ↾ 𝑋) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋)))
25		eleq1 2817	. . . . . . . . . 10 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (𝑒 ∈ (𝑐 × 𝑑) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑)))
26	25	anbi1d 631	. . . . . . . . 9 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
27	26	2rexbidv 3203	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
28	24, 27	imbi12d 344	. . . . . . 7 ⊢ (𝑒 = ⟨𝑎, 𝑏⟩ → ((¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
29	28	ralxp 5808	. . . . . 6 ⊢ (∀𝑒 ∈ (𝑋 × 𝑋)(¬ 𝑒 ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))))
30	22, 29	bitrdi 287	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑒 ∈ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑒 ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))))
31		vex 3454	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
32	31	opelresi 5961	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I ))
33		ibar 528	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑋 → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )))
34	33	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (⟨𝑎, 𝑏⟩ ∈ I ↔ (𝑎 ∈ 𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ I )))
35		df-br 5111	. . . . . . . . . . . 12 ⊢ (𝑎 I 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ I )
36	31	ideq 5819	. . . . . . . . . . . 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 481	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 = 𝑏))
41	40	necon3bbid 2963	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) ↔ 𝑎 ≠ 𝑏))
42		elssuni 4904	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ 𝐽 → 𝑐 ⊆ ∪ 𝐽)
43		elssuni 4904	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝐽 → 𝑑 ⊆ ∪ 𝐽)
44		xpss12 5656	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ⊆ ∪ 𝐽 ∧ 𝑑 ⊆ ∪ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽))
45	42, 43, 44	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (∪ 𝐽 × ∪ 𝐽))
46	1, 1	xpeq12i 5669	. . . . . . . . . . . . . . 15 ⊢ (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽)
47	45, 46	sseqtrrdi 3991	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋))
48	47	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ (𝑋 × 𝑋))
49	7	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
50	48, 49	sseqtrd 3986	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (𝑐 × 𝑑) ⊆ ∪ (𝐽 ×_t 𝐽))
51		reldisj 4419	. . . . . . . . . . . 12 ⊢ ((𝑐 × 𝑑) ⊆ ∪ (𝐽 ×_t 𝐽) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
52	50, 51	syl 17	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
53		df-res 5653	. . . . . . . . . . . . . . 15 ⊢ ( I ↾ 𝑋) = ( I ∩ (𝑋 × V))
54	53	ineq2i 4183	. . . . . . . . . . . . . 14 ⊢ ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V)))
55		inass 4194	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V)))
56		inss1 4203	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑐 × 𝑑)
57	56, 48	sstrid 3961	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × 𝑋))
58		ssv 3974	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑋 ⊆ V
59		xpss2 5661	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ⊆ V → (𝑋 × 𝑋) ⊆ (𝑋 × V))
60	58, 59	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 × 𝑋) ⊆ (𝑋 × V)
61	57, 60	sstrdi 3962	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V))
62		dfss2 3935	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 × 𝑑) ∩ I ) ⊆ (𝑋 × V) ↔ (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I ))
63	61, 62	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ I ) ∩ (𝑋 × V)) = ((𝑐 × 𝑑) ∩ I ))
64	55, 63	eqtr3id 2779	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ∩ (𝑋 × V))) = ((𝑐 × 𝑑) ∩ I ))
65	54, 64	eqtrid 2777	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ((𝑐 × 𝑑) ∩ I ))
66	65	eqeq1d 2732	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → (((𝑐 × 𝑑) ∩ ( I ↾ 𝑋)) = ∅ ↔ ((𝑐 × 𝑑) ∩ I ) = ∅))
67		opelxp 5677	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑))
68		df-br 5111	. . . . . . . . . . . . . . . 16 ⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ ⟨𝑎, 𝑎⟩ ∈ (𝑐 × 𝑑))
69		elin 3933	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (𝑐 ∩ 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑎 ∈ 𝑑))
70	67, 68, 69	3bitr4i 303	. . . . . . . . . . . . . . 15 ⊢ (𝑎(𝑐 × 𝑑)𝑎 ↔ 𝑎 ∈ (𝑐 ∩ 𝑑))
71	70	notbii 320	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑎(𝑐 × 𝑑)𝑎 ↔ ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
72	71	albii 1819	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎 ↔ ∀𝑎 ¬ 𝑎 ∈ (𝑐 ∩ 𝑑))
73		intirr 6094	. . . . . . . . . . . . 13 ⊢ (((𝑐 × 𝑑) ∩ I ) = ∅ ↔ ∀𝑎 ¬ 𝑎(𝑐 × 𝑑)𝑎)
74		eq0 4316	. . . . . . . . . . . . 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 5677	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑))
80	79	anbi1i 624	. . . . . . . . 9 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))))
81		df-3an 1088	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅) ↔ ((𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑) ∧ (𝑐 ∩ 𝑑) = ∅))
82	78, 80, 81	3bitr4g 314	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑐 ∈ 𝐽 ∧ 𝑑 ∈ 𝐽)) → ((⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))
83	82	2rexbidva 3201	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋))) ↔ ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅)))
84	41, 83	imbi12d 344	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((¬ ⟨𝑎, 𝑏⟩ ∈ ( I ↾ 𝑋) → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (⟨𝑎, 𝑏⟩ ∈ (𝑐 × 𝑑) ∧ (𝑐 × 𝑑) ⊆ (∪ (𝐽 ×_t 𝐽) ∖ ( I ↾ 𝑋)))) ↔ (𝑎 ≠ 𝑏 → ∃𝑐 ∈ 𝐽 ∃𝑑 ∈ 𝐽 (𝑎 ∈ 𝑐 ∧ 𝑏 ∈ 𝑑 ∧ (𝑐 ∩ 𝑑) = ∅))))
85	84	2ralbidva 3200	. . . . 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 574	. 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 206 ∧ wa 395 ∧ w3a 1086 ∀wal 1538 = wceq 1540 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 Vcvv 3450 ∖ cdif 3914 ∩ cin 3916 ⊆ wss 3917 ∅c0 4299 ⟨cop 4598 ∪ cuni 4874 class class class wbr 5110 I cid 5535 × cxp 5639 ↾ cres 5643 ‘cfv 6514 (class class class)co 7390 Topctop 22787 Clsdccld 22910 Hauscha 23202 ×_t ctx 23454

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 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-fv 6522 df-ov 7393 df-oprab 7394 df-mpo 7395 df-1st 7971 df-2nd 7972 df-topgen 17413 df-top 22788 df-topon 22805 df-bases 22840 df-cld 22913 df-haus 23209 df-tx 23456

This theorem is referenced by: hauseqlcld 23540 tgphaus 24011 qtophaus 33833

W3C validator