Metamath Proof Explorer


Theorem txhaus

Description: The topological product of two Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Assertion txhaus ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( 𝑅 ×t 𝑆 ) ∈ Haus )

Proof

Step Hyp Ref Expression
1 haustop ( 𝑅 ∈ Haus → 𝑅 ∈ Top )
2 haustop ( 𝑆 ∈ Haus → 𝑆 ∈ Top )
3 txtop ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
4 1 2 3 syl2an ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
5 eqid 𝑅 = 𝑅
6 eqid 𝑆 = 𝑆
7 5 6 txuni ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 × 𝑆 ) = ( 𝑅 ×t 𝑆 ) )
8 1 2 7 syl2an ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( 𝑅 × 𝑆 ) = ( 𝑅 ×t 𝑆 ) )
9 8 eleq2d ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ↔ 𝑥 ( 𝑅 ×t 𝑆 ) ) )
10 8 eleq2d ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( 𝑦 ∈ ( 𝑅 × 𝑆 ) ↔ 𝑦 ( 𝑅 ×t 𝑆 ) ) )
11 9 10 anbi12d ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ↔ ( 𝑥 ( 𝑅 ×t 𝑆 ) ∧ 𝑦 ( 𝑅 ×t 𝑆 ) ) ) )
12 neorian ( ( ( 1st𝑥 ) ≠ ( 1st𝑦 ) ∨ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ↔ ¬ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) )
13 xpopth ( ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) → ( ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ↔ 𝑥 = 𝑦 ) )
14 13 adantl ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → ( ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ↔ 𝑥 = 𝑦 ) )
15 14 necon3bbid ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → ( ¬ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ↔ 𝑥𝑦 ) )
16 12 15 syl5bb ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → ( ( ( 1st𝑥 ) ≠ ( 1st𝑦 ) ∨ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ↔ 𝑥𝑦 ) )
17 simplll ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) → 𝑅 ∈ Haus )
18 xp1st ( 𝑥 ∈ ( 𝑅 × 𝑆 ) → ( 1st𝑥 ) ∈ 𝑅 )
19 18 ad2antrl ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → ( 1st𝑥 ) ∈ 𝑅 )
20 19 adantr ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) → ( 1st𝑥 ) ∈ 𝑅 )
21 xp1st ( 𝑦 ∈ ( 𝑅 × 𝑆 ) → ( 1st𝑦 ) ∈ 𝑅 )
22 21 ad2antll ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → ( 1st𝑦 ) ∈ 𝑅 )
23 22 adantr ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) → ( 1st𝑦 ) ∈ 𝑅 )
24 simpr ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) → ( 1st𝑥 ) ≠ ( 1st𝑦 ) )
25 5 hausnei ( ( 𝑅 ∈ Haus ∧ ( ( 1st𝑥 ) ∈ 𝑅 ∧ ( 1st𝑦 ) ∈ 𝑅 ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ) → ∃ 𝑢𝑅𝑣𝑅 ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) )
26 17 20 23 24 25 syl13anc ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) → ∃ 𝑢𝑅𝑣𝑅 ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) )
27 1 ad2antrr ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → 𝑅 ∈ Top )
28 27 ad2antrr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑅 ∈ Top )
29 2 ad4antlr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑆 ∈ Top )
30 simprll ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑢𝑅 )
31 6 topopn ( 𝑆 ∈ Top → 𝑆𝑆 )
32 29 31 syl ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑆𝑆 )
33 txopn ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑢𝑅 𝑆𝑆 ) ) → ( 𝑢 × 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) )
34 28 29 30 32 33 syl22anc ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 𝑢 × 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) )
35 simprlr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑣𝑅 )
36 txopn ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑣𝑅 𝑆𝑆 ) ) → ( 𝑣 × 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) )
37 28 29 35 32 36 syl22anc ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 𝑣 × 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) )
38 1st2nd2 ( 𝑥 ∈ ( 𝑅 × 𝑆 ) → 𝑥 = ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ )
39 38 ad2antrl ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → 𝑥 = ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ )
40 39 ad2antrr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑥 = ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ )
41 simprr1 ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 1st𝑥 ) ∈ 𝑢 )
42 xp2nd ( 𝑥 ∈ ( 𝑅 × 𝑆 ) → ( 2nd𝑥 ) ∈ 𝑆 )
43 42 ad2antrl ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → ( 2nd𝑥 ) ∈ 𝑆 )
44 43 ad2antrr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 2nd𝑥 ) ∈ 𝑆 )
45 41 44 jca ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑥 ) ∈ 𝑆 ) )
46 elxp6 ( 𝑥 ∈ ( 𝑢 × 𝑆 ) ↔ ( 𝑥 = ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑥 ) ∈ 𝑆 ) ) )
47 40 45 46 sylanbrc ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑥 ∈ ( 𝑢 × 𝑆 ) )
48 1st2nd2 ( 𝑦 ∈ ( 𝑅 × 𝑆 ) → 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
49 48 ad2antll ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
50 49 ad2antrr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
51 simprr2 ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 1st𝑦 ) ∈ 𝑣 )
52 xp2nd ( 𝑦 ∈ ( 𝑅 × 𝑆 ) → ( 2nd𝑦 ) ∈ 𝑆 )
53 52 ad2antll ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → ( 2nd𝑦 ) ∈ 𝑆 )
54 53 ad2antrr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 2nd𝑦 ) ∈ 𝑆 )
55 51 54 jca ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( ( 1st𝑦 ) ∈ 𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑆 ) )
56 elxp6 ( 𝑦 ∈ ( 𝑣 × 𝑆 ) ↔ ( 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ ∧ ( ( 1st𝑦 ) ∈ 𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑆 ) ) )
57 50 55 56 sylanbrc ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑦 ∈ ( 𝑣 × 𝑆 ) )
58 simprr3 ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 𝑢𝑣 ) = ∅ )
59 58 xpeq1d ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( ( 𝑢𝑣 ) × 𝑆 ) = ( ∅ × 𝑆 ) )
60 xpindir ( ( 𝑢𝑣 ) × 𝑆 ) = ( ( 𝑢 × 𝑆 ) ∩ ( 𝑣 × 𝑆 ) )
61 0xp ( ∅ × 𝑆 ) = ∅
62 59 60 61 3eqtr3g ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( ( 𝑢 × 𝑆 ) ∩ ( 𝑣 × 𝑆 ) ) = ∅ )
63 eleq2 ( 𝑧 = ( 𝑢 × 𝑆 ) → ( 𝑥𝑧𝑥 ∈ ( 𝑢 × 𝑆 ) ) )
64 ineq1 ( 𝑧 = ( 𝑢 × 𝑆 ) → ( 𝑧𝑤 ) = ( ( 𝑢 × 𝑆 ) ∩ 𝑤 ) )
65 64 eqeq1d ( 𝑧 = ( 𝑢 × 𝑆 ) → ( ( 𝑧𝑤 ) = ∅ ↔ ( ( 𝑢 × 𝑆 ) ∩ 𝑤 ) = ∅ ) )
66 63 65 3anbi13d ( 𝑧 = ( 𝑢 × 𝑆 ) → ( ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ↔ ( 𝑥 ∈ ( 𝑢 × 𝑆 ) ∧ 𝑦𝑤 ∧ ( ( 𝑢 × 𝑆 ) ∩ 𝑤 ) = ∅ ) ) )
67 eleq2 ( 𝑤 = ( 𝑣 × 𝑆 ) → ( 𝑦𝑤𝑦 ∈ ( 𝑣 × 𝑆 ) ) )
68 ineq2 ( 𝑤 = ( 𝑣 × 𝑆 ) → ( ( 𝑢 × 𝑆 ) ∩ 𝑤 ) = ( ( 𝑢 × 𝑆 ) ∩ ( 𝑣 × 𝑆 ) ) )
69 68 eqeq1d ( 𝑤 = ( 𝑣 × 𝑆 ) → ( ( ( 𝑢 × 𝑆 ) ∩ 𝑤 ) = ∅ ↔ ( ( 𝑢 × 𝑆 ) ∩ ( 𝑣 × 𝑆 ) ) = ∅ ) )
70 67 69 3anbi23d ( 𝑤 = ( 𝑣 × 𝑆 ) → ( ( 𝑥 ∈ ( 𝑢 × 𝑆 ) ∧ 𝑦𝑤 ∧ ( ( 𝑢 × 𝑆 ) ∩ 𝑤 ) = ∅ ) ↔ ( 𝑥 ∈ ( 𝑢 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑣 × 𝑆 ) ∧ ( ( 𝑢 × 𝑆 ) ∩ ( 𝑣 × 𝑆 ) ) = ∅ ) ) )
71 66 70 rspc2ev ( ( ( 𝑢 × 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) ∧ ( 𝑣 × 𝑆 ) ∈ ( 𝑅 ×t 𝑆 ) ∧ ( 𝑥 ∈ ( 𝑢 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑣 × 𝑆 ) ∧ ( ( 𝑢 × 𝑆 ) ∩ ( 𝑣 × 𝑆 ) ) = ∅ ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) )
72 34 37 47 57 62 71 syl113anc ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( ( 𝑢𝑅𝑣𝑅 ) ∧ ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) )
73 72 expr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) ∧ ( 𝑢𝑅𝑣𝑅 ) ) → ( ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ) )
74 73 rexlimdvva ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) → ( ∃ 𝑢𝑅𝑣𝑅 ( ( 1st𝑥 ) ∈ 𝑢 ∧ ( 1st𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ) )
75 26 74 mpd ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 1st𝑥 ) ≠ ( 1st𝑦 ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) )
76 simpllr ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) → 𝑆 ∈ Haus )
77 43 adantr ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) → ( 2nd𝑥 ) ∈ 𝑆 )
78 53 adantr ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) → ( 2nd𝑦 ) ∈ 𝑆 )
79 simpr ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) → ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) )
80 6 hausnei ( ( 𝑆 ∈ Haus ∧ ( ( 2nd𝑥 ) ∈ 𝑆 ∧ ( 2nd𝑦 ) ∈ 𝑆 ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ) → ∃ 𝑢𝑆𝑣𝑆 ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) )
81 76 77 78 79 80 syl13anc ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) → ∃ 𝑢𝑆𝑣𝑆 ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) )
82 27 ad2antrr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑅 ∈ Top )
83 2 ad4antlr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑆 ∈ Top )
84 5 topopn ( 𝑅 ∈ Top → 𝑅𝑅 )
85 82 84 syl ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑅𝑅 )
86 simprll ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑢𝑆 )
87 txopn ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑅𝑅𝑢𝑆 ) ) → ( 𝑅 × 𝑢 ) ∈ ( 𝑅 ×t 𝑆 ) )
88 82 83 85 86 87 syl22anc ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 𝑅 × 𝑢 ) ∈ ( 𝑅 ×t 𝑆 ) )
89 simprlr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑣𝑆 )
90 txopn ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑅𝑅𝑣𝑆 ) ) → ( 𝑅 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) )
91 82 83 85 89 90 syl22anc ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 𝑅 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) )
92 39 ad2antrr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑥 = ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ )
93 19 ad2antrr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 1st𝑥 ) ∈ 𝑅 )
94 simprr1 ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 2nd𝑥 ) ∈ 𝑢 )
95 93 94 jca ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( ( 1st𝑥 ) ∈ 𝑅 ∧ ( 2nd𝑥 ) ∈ 𝑢 ) )
96 elxp6 ( 𝑥 ∈ ( 𝑅 × 𝑢 ) ↔ ( 𝑥 = ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∧ ( ( 1st𝑥 ) ∈ 𝑅 ∧ ( 2nd𝑥 ) ∈ 𝑢 ) ) )
97 92 95 96 sylanbrc ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑥 ∈ ( 𝑅 × 𝑢 ) )
98 49 ad2antrr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
99 22 ad2antrr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 1st𝑦 ) ∈ 𝑅 )
100 simprr2 ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 2nd𝑦 ) ∈ 𝑣 )
101 99 100 jca ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( ( 1st𝑦 ) ∈ 𝑅 ∧ ( 2nd𝑦 ) ∈ 𝑣 ) )
102 elxp6 ( 𝑦 ∈ ( 𝑅 × 𝑣 ) ↔ ( 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ ∧ ( ( 1st𝑦 ) ∈ 𝑅 ∧ ( 2nd𝑦 ) ∈ 𝑣 ) ) )
103 98 101 102 sylanbrc ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → 𝑦 ∈ ( 𝑅 × 𝑣 ) )
104 simprr3 ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 𝑢𝑣 ) = ∅ )
105 104 xpeq2d ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( 𝑅 × ( 𝑢𝑣 ) ) = ( 𝑅 × ∅ ) )
106 xpindi ( 𝑅 × ( 𝑢𝑣 ) ) = ( ( 𝑅 × 𝑢 ) ∩ ( 𝑅 × 𝑣 ) )
107 xp0 ( 𝑅 × ∅ ) = ∅
108 105 106 107 3eqtr3g ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ( ( 𝑅 × 𝑢 ) ∩ ( 𝑅 × 𝑣 ) ) = ∅ )
109 eleq2 ( 𝑧 = ( 𝑅 × 𝑢 ) → ( 𝑥𝑧𝑥 ∈ ( 𝑅 × 𝑢 ) ) )
110 ineq1 ( 𝑧 = ( 𝑅 × 𝑢 ) → ( 𝑧𝑤 ) = ( ( 𝑅 × 𝑢 ) ∩ 𝑤 ) )
111 110 eqeq1d ( 𝑧 = ( 𝑅 × 𝑢 ) → ( ( 𝑧𝑤 ) = ∅ ↔ ( ( 𝑅 × 𝑢 ) ∩ 𝑤 ) = ∅ ) )
112 109 111 3anbi13d ( 𝑧 = ( 𝑅 × 𝑢 ) → ( ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ↔ ( 𝑥 ∈ ( 𝑅 × 𝑢 ) ∧ 𝑦𝑤 ∧ ( ( 𝑅 × 𝑢 ) ∩ 𝑤 ) = ∅ ) ) )
113 eleq2 ( 𝑤 = ( 𝑅 × 𝑣 ) → ( 𝑦𝑤𝑦 ∈ ( 𝑅 × 𝑣 ) ) )
114 ineq2 ( 𝑤 = ( 𝑅 × 𝑣 ) → ( ( 𝑅 × 𝑢 ) ∩ 𝑤 ) = ( ( 𝑅 × 𝑢 ) ∩ ( 𝑅 × 𝑣 ) ) )
115 114 eqeq1d ( 𝑤 = ( 𝑅 × 𝑣 ) → ( ( ( 𝑅 × 𝑢 ) ∩ 𝑤 ) = ∅ ↔ ( ( 𝑅 × 𝑢 ) ∩ ( 𝑅 × 𝑣 ) ) = ∅ ) )
116 113 115 3anbi23d ( 𝑤 = ( 𝑅 × 𝑣 ) → ( ( 𝑥 ∈ ( 𝑅 × 𝑢 ) ∧ 𝑦𝑤 ∧ ( ( 𝑅 × 𝑢 ) ∩ 𝑤 ) = ∅ ) ↔ ( 𝑥 ∈ ( 𝑅 × 𝑢 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑣 ) ∧ ( ( 𝑅 × 𝑢 ) ∩ ( 𝑅 × 𝑣 ) ) = ∅ ) ) )
117 112 116 rspc2ev ( ( ( 𝑅 × 𝑢 ) ∈ ( 𝑅 ×t 𝑆 ) ∧ ( 𝑅 × 𝑣 ) ∈ ( 𝑅 ×t 𝑆 ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑢 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑣 ) ∧ ( ( 𝑅 × 𝑢 ) ∩ ( 𝑅 × 𝑣 ) ) = ∅ ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) )
118 88 91 97 103 108 117 syl113anc ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( ( 𝑢𝑆𝑣𝑆 ) ∧ ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) )
119 118 expr ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ∧ ( 𝑢𝑆𝑣𝑆 ) ) → ( ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ) )
120 119 rexlimdvva ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) → ( ∃ 𝑢𝑆𝑣𝑆 ( ( 2nd𝑥 ) ∈ 𝑢 ∧ ( 2nd𝑦 ) ∈ 𝑣 ∧ ( 𝑢𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ) )
121 81 120 mpd ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) )
122 75 121 jaodan ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) ∧ ( ( 1st𝑥 ) ≠ ( 1st𝑦 ) ∨ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) )
123 122 ex ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → ( ( ( 1st𝑥 ) ≠ ( 1st𝑦 ) ∨ ( 2nd𝑥 ) ≠ ( 2nd𝑦 ) ) → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ) )
124 16 123 sylbird ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) ) → ( 𝑥𝑦 → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ) )
125 124 ex ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( ( 𝑥 ∈ ( 𝑅 × 𝑆 ) ∧ 𝑦 ∈ ( 𝑅 × 𝑆 ) ) → ( 𝑥𝑦 → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ) ) )
126 11 125 sylbird ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( ( 𝑥 ( 𝑅 ×t 𝑆 ) ∧ 𝑦 ( 𝑅 ×t 𝑆 ) ) → ( 𝑥𝑦 → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ) ) )
127 126 ralrimivv ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ∀ 𝑥 ( 𝑅 ×t 𝑆 ) ∀ 𝑦 ( 𝑅 ×t 𝑆 ) ( 𝑥𝑦 → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ) )
128 eqid ( 𝑅 ×t 𝑆 ) = ( 𝑅 ×t 𝑆 )
129 128 ishaus ( ( 𝑅 ×t 𝑆 ) ∈ Haus ↔ ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ∀ 𝑥 ( 𝑅 ×t 𝑆 ) ∀ 𝑦 ( 𝑅 ×t 𝑆 ) ( 𝑥𝑦 → ∃ 𝑧 ∈ ( 𝑅 ×t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑥𝑧𝑦𝑤 ∧ ( 𝑧𝑤 ) = ∅ ) ) ) )
130 4 127 129 sylanbrc ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) → ( 𝑅 ×t 𝑆 ) ∈ Haus )