txconn

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

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

Proof

Step	Hyp	Ref	Expression
1		conntop	$⊢ R \in Conn \to R \in Top$
2		conntop	$⊢ S \in Conn \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 Conn \land S \in Conn) \to R \times_{t} S \in Top$
5		neq0	$⊢ \neg x = \emptyset \leftrightarrow \exists z z \in x$
6		simplr	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land z \in x) \to x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))$
7	6	elin1d	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land z \in x) \to x \in (R \times_{t} S)$
8		elssuni	$⊢ x \in (R \times_{t} S) \to x \subseteq ⋃ (R \times_{t} S)$
9	7 8	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land z \in x) \to x \subseteq ⋃ (R \times_{t} S)$
10		simprr	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to w \in ⋃ (R \times_{t} S)$
11		simplll	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to R \in Conn$
12	11 1	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to R \in Top$
13		simpllr	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to S \in Conn$
14	13 2	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to S \in Top$
15		eqid	$⊢ ⋃ R = ⋃ R$
16		eqid	$⊢ ⋃ S = ⋃ S$
17	15 16	txuni	$⊢ (R \in Top \land S \in Top) \to ⋃ R \times ⋃ S = ⋃ (R \times_{t} S)$
18	12 14 17	syl2anc	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to ⋃ R \times ⋃ S = ⋃ (R \times_{t} S)$
19	10 18	eleqtrrd	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to w \in (⋃ R \times ⋃ S)$
20		1st2nd2	$⊢ w \in (⋃ R \times ⋃ S) \to w = ⟨1^{st} (w), 2^{nd} (w)⟩$
21	19 20	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to w = ⟨1^{st} (w), 2^{nd} (w)⟩$
22		xp2nd	$⊢ w \in (⋃ R \times ⋃ S) \to 2^{nd} (w) \in ⋃ S$
23	19 22	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to 2^{nd} (w) \in ⋃ S$
24		eqid	$⊢ (a \in ⋃ S ⟼ ⟨1^{st} (w), a⟩) = (a \in ⋃ S ⟼ ⟨1^{st} (w), a⟩)$
25	24	mptpreima	$⊢ {(a \in ⋃ S ⟼ ⟨1^{st} (w), a⟩)}^{-1} [x] = \{a \in ⋃ S \| ⟨1^{st} (w), a⟩ \in x\}$
26		toptopon2	$⊢ S \in Top \leftrightarrow S \in TopOn (⋃ S)$
27	14 26	sylib	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to S \in TopOn (⋃ S)$
28		toptopon2	$⊢ R \in Top \leftrightarrow R \in TopOn (⋃ R)$
29	12 28	sylib	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to R \in TopOn (⋃ R)$
30		xp1st	$⊢ w \in (⋃ R \times ⋃ S) \to 1^{st} (w) \in ⋃ R$
31	19 30	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to 1^{st} (w) \in ⋃ R$
32	27 29 31	cnmptc	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to (a \in ⋃ S ⟼ 1^{st} (w)) \in (S Cn R)$
33	27	cnmptid	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to (a \in ⋃ S ⟼ a) \in (S Cn S)$
34	27 32 33	cnmpt1t	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to (a \in ⋃ S ⟼ ⟨1^{st} (w), a⟩) \in (S Cn (R \times_{t} S))$
35		simplr	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))$
36	35	elin1d	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to x \in (R \times_{t} S)$
37		cnima	$⊢ ((a \in ⋃ S ⟼ ⟨1^{st} (w), a⟩) \in (S Cn (R \times_{t} S)) \land x \in (R \times_{t} S)) \to {(a \in ⋃ S ⟼ ⟨1^{st} (w), a⟩)}^{-1} [x] \in S$
38	34 36 37	syl2anc	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to {(a \in ⋃ S ⟼ ⟨1^{st} (w), a⟩)}^{-1} [x] \in S$
39	25 38	eqeltrrid	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to \{a \in ⋃ S \| ⟨1^{st} (w), a⟩ \in x\} \in S$
40		simprl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to z \in x$
41		elunii	$⊢ (z \in x \land x \in (R \times_{t} S)) \to z \in ⋃ (R \times_{t} S)$
42	40 36 41	syl2anc	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to z \in ⋃ (R \times_{t} S)$
43	42 18	eleqtrrd	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to z \in (⋃ R \times ⋃ S)$
44		xp2nd	$⊢ z \in (⋃ R \times ⋃ S) \to 2^{nd} (z) \in ⋃ S$
45	43 44	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to 2^{nd} (z) \in ⋃ S$
46		eqid	$⊢ (a \in ⋃ R ⟼ ⟨a, 2^{nd} (z)⟩) = (a \in ⋃ R ⟼ ⟨a, 2^{nd} (z)⟩)$
47	46	mptpreima	$⊢ {(a \in ⋃ R ⟼ ⟨a, 2^{nd} (z)⟩)}^{-1} [x] = \{a \in ⋃ R \| ⟨a, 2^{nd} (z)⟩ \in x\}$
48	29	cnmptid	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to (a \in ⋃ R ⟼ a) \in (R Cn R)$
49	29 27 45	cnmptc	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to (a \in ⋃ R ⟼ 2^{nd} (z)) \in (R Cn S)$
50	29 48 49	cnmpt1t	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to (a \in ⋃ R ⟼ ⟨a, 2^{nd} (z)⟩) \in (R Cn (R \times_{t} S))$
51		cnima	$⊢ ((a \in ⋃ R ⟼ ⟨a, 2^{nd} (z)⟩) \in (R Cn (R \times_{t} S)) \land x \in (R \times_{t} S)) \to {(a \in ⋃ R ⟼ ⟨a, 2^{nd} (z)⟩)}^{-1} [x] \in R$
52	50 36 51	syl2anc	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to {(a \in ⋃ R ⟼ ⟨a, 2^{nd} (z)⟩)}^{-1} [x] \in R$
53	47 52	eqeltrrid	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to \{a \in ⋃ R \| ⟨a, 2^{nd} (z)⟩ \in x\} \in R$
54		xp1st	$⊢ z \in (⋃ R \times ⋃ S) \to 1^{st} (z) \in ⋃ R$
55	43 54	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to 1^{st} (z) \in ⋃ R$
56		1st2nd2	$⊢ z \in (⋃ R \times ⋃ S) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
57	43 56	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
58	57 40	eqeltrrd	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to ⟨1^{st} (z), 2^{nd} (z)⟩ \in x$
59		opeq1	$⊢ a = 1^{st} (z) \to ⟨a, 2^{nd} (z)⟩ = ⟨1^{st} (z), 2^{nd} (z)⟩$
60	59	eleq1d	$⊢ a = 1^{st} (z) \to (⟨a, 2^{nd} (z)⟩ \in x \leftrightarrow ⟨1^{st} (z), 2^{nd} (z)⟩ \in x)$
61	60	rspcev	$⊢ (1^{st} (z) \in ⋃ R \land ⟨1^{st} (z), 2^{nd} (z)⟩ \in x) \to \exists a \in ⋃ R ⟨a, 2^{nd} (z)⟩ \in x$
62	55 58 61	syl2anc	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to \exists a \in ⋃ R ⟨a, 2^{nd} (z)⟩ \in x$
63		rabn0	$⊢ \{a \in ⋃ R \| ⟨a, 2^{nd} (z)⟩ \in x\} \neq \emptyset \leftrightarrow \exists a \in ⋃ R ⟨a, 2^{nd} (z)⟩ \in x$
64	62 63	sylibr	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to \{a \in ⋃ R \| ⟨a, 2^{nd} (z)⟩ \in x\} \neq \emptyset$
65	35	elin2d	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to x \in Clsd (R \times_{t} S)$
66		cnclima	$⊢ ((a \in ⋃ R ⟼ ⟨a, 2^{nd} (z)⟩) \in (R Cn (R \times_{t} S)) \land x \in Clsd (R \times_{t} S)) \to {(a \in ⋃ R ⟼ ⟨a, 2^{nd} (z)⟩)}^{-1} [x] \in Clsd (R)$
67	50 65 66	syl2anc	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to {(a \in ⋃ R ⟼ ⟨a, 2^{nd} (z)⟩)}^{-1} [x] \in Clsd (R)$
68	47 67	eqeltrrid	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to \{a \in ⋃ R \| ⟨a, 2^{nd} (z)⟩ \in x\} \in Clsd (R)$
69	15 11 53 64 68	connclo	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to \{a \in ⋃ R \| ⟨a, 2^{nd} (z)⟩ \in x\} = ⋃ R$
70	31 69	eleqtrrd	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to 1^{st} (w) \in \{a \in ⋃ R \| ⟨a, 2^{nd} (z)⟩ \in x\}$
71		opeq1	$⊢ a = 1^{st} (w) \to ⟨a, 2^{nd} (z)⟩ = ⟨1^{st} (w), 2^{nd} (z)⟩$
72	71	eleq1d	$⊢ a = 1^{st} (w) \to (⟨a, 2^{nd} (z)⟩ \in x \leftrightarrow ⟨1^{st} (w), 2^{nd} (z)⟩ \in x)$
73	72	elrab	$⊢ 1^{st} (w) \in \{a \in ⋃ R \| ⟨a, 2^{nd} (z)⟩ \in x\} \leftrightarrow (1^{st} (w) \in ⋃ R \land ⟨1^{st} (w), 2^{nd} (z)⟩ \in x)$
74	73	simprbi	$⊢ 1^{st} (w) \in \{a \in ⋃ R \| ⟨a, 2^{nd} (z)⟩ \in x\} \to ⟨1^{st} (w), 2^{nd} (z)⟩ \in x$
75	70 74	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to ⟨1^{st} (w), 2^{nd} (z)⟩ \in x$
76		opeq2	$⊢ a = 2^{nd} (z) \to ⟨1^{st} (w), a⟩ = ⟨1^{st} (w), 2^{nd} (z)⟩$
77	76	eleq1d	$⊢ a = 2^{nd} (z) \to (⟨1^{st} (w), a⟩ \in x \leftrightarrow ⟨1^{st} (w), 2^{nd} (z)⟩ \in x)$
78	77	rspcev	$⊢ (2^{nd} (z) \in ⋃ S \land ⟨1^{st} (w), 2^{nd} (z)⟩ \in x) \to \exists a \in ⋃ S ⟨1^{st} (w), a⟩ \in x$
79	45 75 78	syl2anc	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to \exists a \in ⋃ S ⟨1^{st} (w), a⟩ \in x$
80		rabn0	$⊢ \{a \in ⋃ S \| ⟨1^{st} (w), a⟩ \in x\} \neq \emptyset \leftrightarrow \exists a \in ⋃ S ⟨1^{st} (w), a⟩ \in x$
81	79 80	sylibr	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to \{a \in ⋃ S \| ⟨1^{st} (w), a⟩ \in x\} \neq \emptyset$
82		cnclima	$⊢ ((a \in ⋃ S ⟼ ⟨1^{st} (w), a⟩) \in (S Cn (R \times_{t} S)) \land x \in Clsd (R \times_{t} S)) \to {(a \in ⋃ S ⟼ ⟨1^{st} (w), a⟩)}^{-1} [x] \in Clsd (S)$
83	34 65 82	syl2anc	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to {(a \in ⋃ S ⟼ ⟨1^{st} (w), a⟩)}^{-1} [x] \in Clsd (S)$
84	25 83	eqeltrrid	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to \{a \in ⋃ S \| ⟨1^{st} (w), a⟩ \in x\} \in Clsd (S)$
85	16 13 39 81 84	connclo	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to \{a \in ⋃ S \| ⟨1^{st} (w), a⟩ \in x\} = ⋃ S$
86	23 85	eleqtrrd	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to 2^{nd} (w) \in \{a \in ⋃ S \| ⟨1^{st} (w), a⟩ \in x\}$
87		opeq2	$⊢ a = 2^{nd} (w) \to ⟨1^{st} (w), a⟩ = ⟨1^{st} (w), 2^{nd} (w)⟩$
88	87	eleq1d	$⊢ a = 2^{nd} (w) \to (⟨1^{st} (w), a⟩ \in x \leftrightarrow ⟨1^{st} (w), 2^{nd} (w)⟩ \in x)$
89	88	elrab	$⊢ 2^{nd} (w) \in \{a \in ⋃ S \| ⟨1^{st} (w), a⟩ \in x\} \leftrightarrow (2^{nd} (w) \in ⋃ S \land ⟨1^{st} (w), 2^{nd} (w)⟩ \in x)$
90	89	simprbi	$⊢ 2^{nd} (w) \in \{a \in ⋃ S \| ⟨1^{st} (w), a⟩ \in x\} \to ⟨1^{st} (w), 2^{nd} (w)⟩ \in x$
91	86 90	syl	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to ⟨1^{st} (w), 2^{nd} (w)⟩ \in x$
92	21 91	eqeltrd	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land (z \in x \land w \in ⋃ (R \times_{t} S))) \to w \in x$
93	92	expr	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land z \in x) \to (w \in ⋃ (R \times_{t} S) \to w \in x)$
94	93	ssrdv	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land z \in x) \to ⋃ (R \times_{t} S) \subseteq x$
95	9 94	eqssd	$⊢ (((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \land z \in x) \to x = ⋃ (R \times_{t} S)$
96	95	ex	$⊢ ((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \to (z \in x \to x = ⋃ (R \times_{t} S))$
97	96	exlimdv	$⊢ ((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \to (\exists z z \in x \to x = ⋃ (R \times_{t} S))$
98	5 97	biimtrid	$⊢ ((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \to (\neg x = \emptyset \to x = ⋃ (R \times_{t} S))$
99	98	orrd	$⊢ ((R \in Conn \land S \in Conn) \land x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S))) \to (x = \emptyset \lor x = ⋃ (R \times_{t} S))$
100	99	ex	$⊢ (R \in Conn \land S \in Conn) \to (x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S)) \to (x = \emptyset \lor x = ⋃ (R \times_{t} S)))$
101		vex	$⊢ x \in V$
102	101	elpr	$⊢ x \in \{\emptyset, ⋃ (R \times_{t} S)\} \leftrightarrow (x = \emptyset \lor x = ⋃ (R \times_{t} S))$
103	100 102	imbitrrdi	$⊢ (R \in Conn \land S \in Conn) \to (x \in ((R \times_{t} S) \cap Clsd (R \times_{t} S)) \to x \in \{\emptyset, ⋃ (R \times_{t} S)\})$
104	103	ssrdv	$⊢ (R \in Conn \land S \in Conn) \to (R \times_{t} S) \cap Clsd (R \times_{t} S) \subseteq \{\emptyset, ⋃ (R \times_{t} S)\}$
105		eqid	$⊢ ⋃ (R \times_{t} S) = ⋃ (R \times_{t} S)$
106	105	isconn2	$⊢ R \times_{t} S \in Conn \leftrightarrow (R \times_{t} S \in Top \land (R \times_{t} S) \cap Clsd (R \times_{t} S) \subseteq \{\emptyset, ⋃ (R \times_{t} S)\})$
107	4 104 106	sylanbrc	$⊢ (R \in Conn \land S \in Conn) \to R \times_{t} S \in Conn$

Metamath Proof Explorer

Theorem txconn

Proof