Theorem 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	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		xpexr2	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
2	1	simpld	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐴 ∈ V )
3	1	simprd	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐵 ∈ V )
4		simpr	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐴 × 𝐵 ) ≠ ∅ )
5		xpnz	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
6	4 5	sylibr	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
7	6	simprd	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐵 ≠ ∅ )
8		xpdom3	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐵 ≠ ∅ ) → 𝐴 ≼ ( 𝐴 × 𝐵 ) )
9	2 3 7 8	syl3anc	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐴 ≼ ( 𝐴 × 𝐵 ) )
10		domfi	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ 𝐴 ≼ ( 𝐴 × 𝐵 ) ) → 𝐴 ∈ Fin )
11	9 10	syldan	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐴 ∈ Fin )
12	6	simpld	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐴 ≠ ∅ )
13		xpdom3	⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ) → 𝐵 ≼ ( 𝐵 × 𝐴 ) )
14	3 2 12 13	syl3anc	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐵 ≼ ( 𝐵 × 𝐴 ) )
15		xpcomeng	⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 × 𝐵 ) )
16	3 2 15	syl2anc	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 × 𝐵 ) )
17		domentr	⊢ ( ( 𝐵 ≼ ( 𝐵 × 𝐴 ) ∧ ( 𝐵 × 𝐴 ) ≈ ( 𝐴 × 𝐵 ) ) → 𝐵 ≼ ( 𝐴 × 𝐵 ) )
18	14 16 17	syl2anc	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐵 ≼ ( 𝐴 × 𝐵 ) )
19		domfi	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ 𝐵 ≼ ( 𝐴 × 𝐵 ) ) → 𝐵 ∈ Fin )
20	18 19	syldan	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐵 ∈ Fin )
21	11 20	jca	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )