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 
|- ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( A e. Fin /\ B e. Fin ) )

Proof

Step Hyp Ref Expression
1 xpexr2 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( A e. _V /\ B e. _V ) )
2 1 simpld 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> A e. _V )
3 1 simprd 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> B e. _V )
4 simpr 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( A X. B ) =/= (/) )
5 xpnz 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
6 4 5 sylibr 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( A =/= (/) /\ B =/= (/) ) )
7 6 simprd 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> B =/= (/) )
8 xpdom3 
 |-  ( ( A e. _V /\ B e. _V /\ B =/= (/) ) -> A ~<_ ( A X. B ) )
9 2 3 7 8 syl3anc 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> A ~<_ ( A X. B ) )
10 domfi 
 |-  ( ( ( A X. B ) e. Fin /\ A ~<_ ( A X. B ) ) -> A e. Fin )
11 9 10 syldan 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> A e. Fin )
12 6 simpld 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> A =/= (/) )
13 xpdom3 
 |-  ( ( B e. _V /\ A e. _V /\ A =/= (/) ) -> B ~<_ ( B X. A ) )
14 3 2 12 13 syl3anc 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> B ~<_ ( B X. A ) )
15 xpcomeng 
 |-  ( ( B e. _V /\ A e. _V ) -> ( B X. A ) ~~ ( A X. B ) )
16 3 2 15 syl2anc 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( B X. A ) ~~ ( A X. B ) )
17 domentr 
 |-  ( ( B ~<_ ( B X. A ) /\ ( B X. A ) ~~ ( A X. B ) ) -> B ~<_ ( A X. B ) )
18 14 16 17 syl2anc 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> B ~<_ ( A X. B ) )
19 domfi 
 |-  ( ( ( A X. B ) e. Fin /\ B ~<_ ( A X. B ) ) -> B e. Fin )
20 18 19 syldan 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> B e. Fin )
21 11 20 jca 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( A e. Fin /\ B e. Fin ) )