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	⊢ ( ( ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ↔ ¬ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) )
13		xpopth	⊢ ( ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) → ( ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ↔ 𝑥 = 𝑦 ) )
14	13	adantl	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ↔ 𝑥 = 𝑦 ) )
15	14	necon3bbid	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( ¬ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ↔ 𝑥 ≠ 𝑦 ) )
16	12 15	syl5bb	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( ( ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ↔ 𝑥 ≠ 𝑦 ) )
17		simplll	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) → 𝑅 ∈ Haus )
18		xp1st	⊢ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 1^st ‘ 𝑥 ) ∈ ∪ 𝑅 )
19	18	ad2antrl	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( 1^st ‘ 𝑥 ) ∈ ∪ 𝑅 )
20	19	adantr	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) → ( 1^st ‘ 𝑥 ) ∈ ∪ 𝑅 )
21		xp1st	⊢ ( 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 1^st ‘ 𝑦 ) ∈ ∪ 𝑅 )
22	21	ad2antll	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( 1^st ‘ 𝑦 ) ∈ ∪ 𝑅 )
23	22	adantr	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) → ( 1^st ‘ 𝑦 ) ∈ ∪ 𝑅 )
24		simpr	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) → ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) )
25	5	hausnei	⊢ ( ( 𝑅 ∈ Haus ∧ ( ( 1^st ‘ 𝑥 ) ∈ ∪ 𝑅 ∧ ( 1^st ‘ 𝑦 ) ∈ ∪ 𝑅 ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ) → ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑅 ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
26	17 20 23 24 25	syl13anc	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑅 ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
27	1	ad2antrr	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → 𝑅 ∈ Top )
28	27	ad2antrr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑅 ∈ Top )
29	2	ad4antlr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑆 ∈ Top )
30		simprll	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑢 ∈ 𝑅 )
31	6	topopn	⊢ ( 𝑆 ∈ Top → ∪ 𝑆 ∈ 𝑆 )
32	29 31	syl	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ∪ 𝑆 ∈ 𝑆 )
33		txopn	⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑢 ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆 ) ) → ( 𝑢 × ∪ 𝑆 ) ∈ ( 𝑅 ×_t 𝑆 ) )
34	28 29 30 32 33	syl22anc	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑢 × ∪ 𝑆 ) ∈ ( 𝑅 ×_t 𝑆 ) )
35		simprlr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑣 ∈ 𝑅 )
36		txopn	⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑣 ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆 ) ) → ( 𝑣 × ∪ 𝑆 ) ∈ ( 𝑅 ×_t 𝑆 ) )
37	28 29 35 32 36	syl22anc	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑣 × ∪ 𝑆 ) ∈ ( 𝑅 ×_t 𝑆 ) )
38		1st2nd2	⊢ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
39	38	ad2antrl	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
40	39	ad2antrr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
41		simprr1	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 1^st ‘ 𝑥 ) ∈ 𝑢 )
42		xp2nd	⊢ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 2^nd ‘ 𝑥 ) ∈ ∪ 𝑆 )
43	42	ad2antrl	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( 2^nd ‘ 𝑥 ) ∈ ∪ 𝑆 )
44	43	ad2antrr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 2^nd ‘ 𝑥 ) ∈ ∪ 𝑆 )
45	41 44	jca	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑥 ) ∈ ∪ 𝑆 ) )
46		elxp6	⊢ ( 𝑥 ∈ ( 𝑢 × ∪ 𝑆 ) ↔ ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑥 ) ∈ ∪ 𝑆 ) ) )
47	40 45 46	sylanbrc	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑥 ∈ ( 𝑢 × ∪ 𝑆 ) )
48		1st2nd2	⊢ ( 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
49	48	ad2antll	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
50	49	ad2antrr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
51		simprr2	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 1^st ‘ 𝑦 ) ∈ 𝑣 )
52		xp2nd	⊢ ( 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 2^nd ‘ 𝑦 ) ∈ ∪ 𝑆 )
53	52	ad2antll	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( 2^nd ‘ 𝑦 ) ∈ ∪ 𝑆 )
54	53	ad2antrr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 2^nd ‘ 𝑦 ) ∈ ∪ 𝑆 )
55	51 54	jca	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ ∪ 𝑆 ) )
56		elxp6	⊢ ( 𝑦 ∈ ( 𝑣 × ∪ 𝑆 ) ↔ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ ∪ 𝑆 ) ) )
57	50 55 56	sylanbrc	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑦 ∈ ( 𝑣 × ∪ 𝑆 ) )
58		simprr3	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑢 ∩ 𝑣 ) = ∅ )
59	58	xpeq1d	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 𝑢 ∩ 𝑣 ) × ∪ 𝑆 ) = ( ∅ × ∪ 𝑆 ) )
60		xpindir	⊢ ( ( 𝑢 ∩ 𝑣 ) × ∪ 𝑆 ) = ( ( 𝑢 × ∪ 𝑆 ) ∩ ( 𝑣 × ∪ 𝑆 ) )
61		0xp	⊢ ( ∅ × ∪ 𝑆 ) = ∅
62	59 60 61	3eqtr3g	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 𝑢 × ∪ 𝑆 ) ∩ ( 𝑣 × ∪ 𝑆 ) ) = ∅ )
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 ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ∃ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )
73	72	expr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) ) → ( ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
74	73	rexlimdvva	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) → ( ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑅 ( ( 1^st ‘ 𝑥 ) ∈ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
75	26 74	mpd	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )
76		simpllr	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) → 𝑆 ∈ Haus )
77	43	adantr	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) → ( 2^nd ‘ 𝑥 ) ∈ ∪ 𝑆 )
78	53	adantr	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) → ( 2^nd ‘ 𝑦 ) ∈ ∪ 𝑆 )
79		simpr	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) → ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) )
80	6	hausnei	⊢ ( ( 𝑆 ∈ Haus ∧ ( ( 2^nd ‘ 𝑥 ) ∈ ∪ 𝑆 ∧ ( 2^nd ‘ 𝑦 ) ∈ ∪ 𝑆 ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ) → ∃ 𝑢 ∈ 𝑆 ∃ 𝑣 ∈ 𝑆 ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
81	76 77 78 79 80	syl13anc	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑆 ∃ 𝑣 ∈ 𝑆 ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
82	27	ad2antrr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑅 ∈ Top )
83	2	ad4antlr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑆 ∈ Top )
84	5	topopn	⊢ ( 𝑅 ∈ Top → ∪ 𝑅 ∈ 𝑅 )
85	82 84	syl	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ∪ 𝑅 ∈ 𝑅 )
86		simprll	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑢 ∈ 𝑆 )
87		txopn	⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( ∪ 𝑅 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) → ( ∪ 𝑅 × 𝑢 ) ∈ ( 𝑅 ×_t 𝑆 ) )
88	82 83 85 86 87	syl22anc	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ∪ 𝑅 × 𝑢 ) ∈ ( 𝑅 ×_t 𝑆 ) )
89		simprlr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑣 ∈ 𝑆 )
90		txopn	⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( ∪ 𝑅 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) → ( ∪ 𝑅 × 𝑣 ) ∈ ( 𝑅 ×_t 𝑆 ) )
91	82 83 85 89 90	syl22anc	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ∪ 𝑅 × 𝑣 ) ∈ ( 𝑅 ×_t 𝑆 ) )
92	39	ad2antrr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
93	19	ad2antrr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 1^st ‘ 𝑥 ) ∈ ∪ 𝑅 )
94		simprr1	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 2^nd ‘ 𝑥 ) ∈ 𝑢 )
95	93 94	jca	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 1^st ‘ 𝑥 ) ∈ ∪ 𝑅 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ) )
96		elxp6	⊢ ( 𝑥 ∈ ( ∪ 𝑅 × 𝑢 ) ↔ ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ ∪ 𝑅 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ) ) )
97	92 95 96	sylanbrc	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑥 ∈ ( ∪ 𝑅 × 𝑢 ) )
98	49	ad2antrr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
99	22	ad2antrr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 1^st ‘ 𝑦 ) ∈ ∪ 𝑅 )
100		simprr2	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 2^nd ‘ 𝑦 ) ∈ 𝑣 )
101	99 100	jca	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( 1^st ‘ 𝑦 ) ∈ ∪ 𝑅 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ) )
102		elxp6	⊢ ( 𝑦 ∈ ( ∪ 𝑅 × 𝑣 ) ↔ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∧ ( ( 1^st ‘ 𝑦 ) ∈ ∪ 𝑅 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ) ) )
103	98 101 102	sylanbrc	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → 𝑦 ∈ ( ∪ 𝑅 × 𝑣 ) )
104		simprr3	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( 𝑢 ∩ 𝑣 ) = ∅ )
105	104	xpeq2d	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ∪ 𝑅 × ( 𝑢 ∩ 𝑣 ) ) = ( ∪ 𝑅 × ∅ ) )
106		xpindi	⊢ ( ∪ 𝑅 × ( 𝑢 ∩ 𝑣 ) ) = ( ( ∪ 𝑅 × 𝑢 ) ∩ ( ∪ 𝑅 × 𝑣 ) )
107		xp0	⊢ ( ∪ 𝑅 × ∅ ) = ∅
108	105 106 107	3eqtr3g	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ( ( ∪ 𝑅 × 𝑢 ) ∩ ( ∪ 𝑅 × 𝑣 ) ) = ∅ )
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 ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ∧ ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ) ) → ∃ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )
119	118	expr	⊢ ( ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
120	119	rexlimdvva	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) → ( ∃ 𝑢 ∈ 𝑆 ∃ 𝑣 ∈ 𝑆 ( ( 2^nd ‘ 𝑥 ) ∈ 𝑢 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
121	81 120	mpd	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )
122	75 121	jaodan	⊢ ( ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) ∧ ( ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) ) → ∃ 𝑧 ∈ ( 𝑅 ×_t 𝑆 ) ∃ 𝑤 ∈ ( 𝑅 ×_t 𝑆 ) ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )
123	122	ex	⊢ ( ( ( 𝑅 ∈ Haus ∧ 𝑆 ∈ Haus ) ∧ ( 𝑥 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) ) ) → ( ( ( 1^st ‘ 𝑥 ) ≠ ( 1^st ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) ≠ ( 2^nd ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝑅 ×_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 )

Metamath Proof Explorer

Theorem txhaus

Proof