txhaus

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

		Ref	Expression
	Assertion	txhaus	$⊢ (R \in Haus \land S \in Haus) \to R \times_{t} S \in Haus$

Proof

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

Metamath Proof Explorer

Theorem txhaus

Proof