Theorem ishaus 23448

Description: The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007.)

Hypothesis

Ref	Expression
ist0.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
ishaus	⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))

Distinct variable groups:   𝑥,𝑦   𝑚,𝑛,𝑥,𝑦,𝐽   𝑥,𝑋,𝑦

Allowed substitution hints:   𝑋(𝑚,𝑛)

Proof of Theorem ishaus

Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4887	. . . 4 ⊢ (𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽)
2		ist0.1	. . . 4 ⊢ 𝑋 = ∪ 𝐽
3	1, 2	eqtr4di 2822	. . 3 ⊢ (𝑗 = 𝐽 → ∪ 𝑗 = 𝑋)
4		rexeq 3325	. . . . . 6 ⊢ (𝑗 = 𝐽 → (∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) ↔ ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))
5	4	rexeqbi1dv 3340	. . . . 5 ⊢ (𝑗 = 𝐽 → (∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) ↔ ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))
6	5	imbi2d 343	. . . 4 ⊢ (𝑗 = 𝐽 → ((𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) ↔ (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
7	3, 6	raleqbidv 3345	. . 3 ⊢ (𝑗 = 𝐽 → (∀𝑦 ∈ ∪ 𝑗(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) ↔ ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
8	3, 7	raleqbidv 3345	. 2 ⊢ (𝑗 = 𝐽 → (∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
9		df-haus 23441	. 2 ⊢ Haus = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝑗 ∃𝑚 ∈ 𝑗 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))}
10	8, 9	elrab2 3663	1 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095   ∩ cin 3912  ∅c0 4294  ∪ cuni 4876  Topctop 23019  Hauscha 23434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-ss 3930  df-uni 4877  df-haus 23441

This theorem is referenced by:  hausnei  23454  haustop  23457  ishaus2  23477  cnhaus  23480  dishaus  23508  pthaus  23764  hausdiag  23771  txhaus  23773  xkohaus  23779