txcmpb

Description: The topological product of two nonempty topologies is compact iff the component topologies are both compact. (Contributed by Mario Carneiro, 14-Sep-2014)

	Ref	Expression
Hypotheses	txcmpb.1	$⊢ X = ⋃ R$
	txcmpb.2	$⊢ Y = ⋃ S$
Assertion	txcmpb	$⊢ ((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (R \times_{t} S \in Comp \leftrightarrow (R \in Comp \land S \in Comp))$

Proof

Step	Hyp	Ref	Expression
1		txcmpb.1	$⊢ X = ⋃ R$
2		txcmpb.2	$⊢ Y = ⋃ S$
3		simpr	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to R \times_{t} S \in Comp$
4		simplrr	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to Y \neq \emptyset$
5		fo1stres	$⊢ Y \neq \emptyset \to ({1^{st} ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} X$
6	4 5	syl	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to ({1^{st} ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} X$
7	1 2	txuni	$⊢ (R \in Top \land S \in Top) \to X \times Y = ⋃ (R \times_{t} S)$
8	7	ad2antrr	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to X \times Y = ⋃ (R \times_{t} S)$
9		foeq2	$⊢ X \times Y = ⋃ (R \times_{t} S) \to (({1^{st} ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} X \leftrightarrow ({1^{st} ↾}_{(X \times Y)}) : ⋃ (R \times_{t} S) \underset{onto}{⟶} X)$
10	8 9	syl	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to (({1^{st} ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} X \leftrightarrow ({1^{st} ↾}_{(X \times Y)}) : ⋃ (R \times_{t} S) \underset{onto}{⟶} X)$
11	6 10	mpbid	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to ({1^{st} ↾}_{(X \times Y)}) : ⋃ (R \times_{t} S) \underset{onto}{⟶} X$
12	1	toptopon	$⊢ R \in Top \leftrightarrow R \in TopOn (X)$
13	2	toptopon	$⊢ S \in Top \leftrightarrow S \in TopOn (Y)$
14		tx1cn	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to {1^{st} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn R)$
15	12 13 14	syl2anb	$⊢ (R \in Top \land S \in Top) \to {1^{st} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn R)$
16	15	ad2antrr	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to {1^{st} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn R)$
17	1	cncmp	$⊢ (R \times_{t} S \in Comp \land ({1^{st} ↾}_{(X \times Y)}) : ⋃ (R \times_{t} S) \underset{onto}{⟶} X \land {1^{st} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn R)) \to R \in Comp$
18	3 11 16 17	syl3anc	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to R \in Comp$
19		simplrl	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to X \neq \emptyset$
20		fo2ndres	$⊢ X \neq \emptyset \to ({2^{nd} ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Y$
21	19 20	syl	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to ({2^{nd} ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Y$
22		foeq2	$⊢ X \times Y = ⋃ (R \times_{t} S) \to (({2^{nd} ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Y \leftrightarrow ({2^{nd} ↾}_{(X \times Y)}) : ⋃ (R \times_{t} S) \underset{onto}{⟶} Y)$
23	8 22	syl	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to (({2^{nd} ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Y \leftrightarrow ({2^{nd} ↾}_{(X \times Y)}) : ⋃ (R \times_{t} S) \underset{onto}{⟶} Y)$
24	21 23	mpbid	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to ({2^{nd} ↾}_{(X \times Y)}) : ⋃ (R \times_{t} S) \underset{onto}{⟶} Y$
25		tx2cn	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to {2^{nd} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn S)$
26	12 13 25	syl2anb	$⊢ (R \in Top \land S \in Top) \to {2^{nd} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn S)$
27	26	ad2antrr	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to {2^{nd} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn S)$
28	2	cncmp	$⊢ (R \times_{t} S \in Comp \land ({2^{nd} ↾}_{(X \times Y)}) : ⋃ (R \times_{t} S) \underset{onto}{⟶} Y \land {2^{nd} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn S)) \to S \in Comp$
29	3 24 27 28	syl3anc	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to S \in Comp$
30	18 29	jca	$⊢ (((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \land R \times_{t} S \in Comp) \to (R \in Comp \land S \in Comp)$
31	30	ex	$⊢ ((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (R \times_{t} S \in Comp \to (R \in Comp \land S \in Comp))$
32		txcmp	$⊢ (R \in Comp \land S \in Comp) \to R \times_{t} S \in Comp$
33	31 32	impbid1	$⊢ ((R \in Top \land S \in Top) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (R \times_{t} S \in Comp \leftrightarrow (R \in Comp \land S \in Comp))$

Metamath Proof Explorer

Theorem txcmpb

Proof