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