This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )