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		xpnz	$⊢ (A \neq \emptyset \land B \neq \emptyset) \leftrightarrow A \times B \neq \emptyset$
5	4	bilanri	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to (A \neq \emptyset \land B \neq \emptyset)$
6	5	simprd	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to B \neq \emptyset$
7		xpdom3	$⊢ (A \in V \land B \in V \land B \neq \emptyset) \to A ≼ (A \times B)$
8	2 3 6 7	syl3anc	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to A ≼ (A \times B)$
9		domfi	$⊢ (A \times B \in Fin \land A ≼ (A \times B)) \to A \in Fin$
10	8 9	syldan	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to A \in Fin$
11	5	simpld	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to A \neq \emptyset$
12		xpdom3	$⊢ (B \in V \land A \in V \land A \neq \emptyset) \to B ≼ (B \times A)$
13	3 2 11 12	syl3anc	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to B ≼ (B \times A)$
14		xpcomeng	$⊢ (B \in V \land A \in V) \to (B \times A) \approx (A \times B)$
15	3 2 14	syl2anc	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to (B \times A) \approx (A \times B)$
16		domentr	$⊢ (B ≼ (B \times A) \land (B \times A) \approx (A \times B)) \to B ≼ (A \times B)$
17	13 15 16	syl2anc	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to B ≼ (A \times B)$
18		domfi	$⊢ (A \times B \in Fin \land B ≼ (A \times B)) \to B \in Fin$
19	17 18	syldan	$⊢ (A \times B \in Fin \land A \times B \neq \emptyset) \to B \in Fin$
20	10 19	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