xpfir

Description: The components of a nonempty finite Cartesian product are finite. (Contributed by Paul Chapman, 11-Apr-2009) (Proof shortened by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	xpfir	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to (A \in Fin \land B \in Fin)$

Proof

Step	Hyp	Ref	Expression
1		xpexr2	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to (A \in V \land B \in V)$
2	1	simpld	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to A \in V$
3	1	simprd	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to B \in V$
4		simpr	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to A \times B \neq \emptyset$
5		xpnz	$⊢ (A \neq \emptyset \land B \neq \emptyset) \leftrightarrow A \times B \neq \emptyset$
6	4 5	sylibr	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to (A \neq \emptyset \land B \neq \emptyset)$
7	6	simprd	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to B \neq \emptyset$
8		xpdom3	$⊢ (A \in V \land B \in V \land B \neq \emptyset) \to A ≼ (A \times B)$
9	2 3 7 8	syl3anc	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to A ≼ (A \times B)$
10		domfi	$⊢ (A \times B \in Fin \land A ≼ (A \times B)) \to A \in Fin$
11	9 10	syldan	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to A \in Fin$
12	6	simpld	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to A \neq \emptyset$
13		xpdom3	$⊢ (B \in V \land A \in V \land A \neq \emptyset) \to B ≼ (B \times A)$
14	3 2 12 13	syl3anc	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to B ≼ (B \times A)$
15		xpcomeng	$⊢ (B \in V \land A \in V) \to (B \times A) \approx (A \times B)$
16	3 2 15	syl2anc	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to (B \times A) \approx (A \times B)$
17		domentr	$⊢ (B ≼ (B \times A) \land (B \times A) \approx (A \times B)) \to B ≼ (A \times B)$
18	14 16 17	syl2anc	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to B ≼ (A \times B)$
19		domfi	$⊢ (A \times B \in Fin \land B ≼ (A \times B)) \to B \in Fin$
20	18 19	syldan	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to B \in Fin$
21	11 20	jca	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to (A \in Fin \land B \in Fin)$

Metamath Proof Explorer

Theorem xpfir

Proof