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		xpnz	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
5	4	bilanri	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
6	5	simprd	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐵 ≠ ∅ )
7		xpdom3	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐵 ≠ ∅ ) → 𝐴 ≼ ( 𝐴 × 𝐵 ) )
8	2 3 6 7	syl3anc	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐴 ≼ ( 𝐴 × 𝐵 ) )
9		domfi	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ 𝐴 ≼ ( 𝐴 × 𝐵 ) ) → 𝐴 ∈ Fin )
10	8 9	syldan	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐴 ∈ Fin )
11	5	simpld	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐴 ≠ ∅ )
12		xpdom3	⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ) → 𝐵 ≼ ( 𝐵 × 𝐴 ) )
13	3 2 11 12	syl3anc	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐵 ≼ ( 𝐵 × 𝐴 ) )
14		xpcomeng	⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 × 𝐵 ) )
15	3 2 14	syl2anc	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 × 𝐵 ) )
16		domentr	⊢ ( ( 𝐵 ≼ ( 𝐵 × 𝐴 ) ∧ ( 𝐵 × 𝐴 ) ≈ ( 𝐴 × 𝐵 ) ) → 𝐵 ≼ ( 𝐴 × 𝐵 ) )
17	13 15 16	syl2anc	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐵 ≼ ( 𝐴 × 𝐵 ) )
18		domfi	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ 𝐵 ≼ ( 𝐴 × 𝐵 ) ) → 𝐵 ∈ Fin )
19	17 18	syldan	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐵 ∈ Fin )
20	10 19	jca	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )