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 xpnz 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
5 4 bilanri 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( A =/= (/) /\ B =/= (/) ) )
6 5 simprd 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> B =/= (/) )
7 xpdom3 
 |-  ( ( A e. _V /\ B e. _V /\ B =/= (/) ) -> A ~<_ ( A X. B ) )
8 2 3 6 7 syl3anc 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> A ~<_ ( A X. B ) )
9 domfi 
 |-  ( ( ( A X. B ) e. Fin /\ A ~<_ ( A X. B ) ) -> A e. Fin )
10 8 9 syldan 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> A e. Fin )
11 5 simpld 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> A =/= (/) )
12 xpdom3 
 |-  ( ( B e. _V /\ A e. _V /\ A =/= (/) ) -> B ~<_ ( B X. A ) )
13 3 2 11 12 syl3anc 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> B ~<_ ( B X. A ) )
14 xpcomeng 
 |-  ( ( B e. _V /\ A e. _V ) -> ( B X. A ) ~~ ( A X. B ) )
15 3 2 14 syl2anc 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( B X. A ) ~~ ( A X. B ) )
16 domentr 
 |-  ( ( B ~<_ ( B X. A ) /\ ( B X. A ) ~~ ( A X. B ) ) -> B ~<_ ( A X. B ) )
17 13 15 16 syl2anc 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> B ~<_ ( A X. B ) )
18 domfi 
 |-  ( ( ( A X. B ) e. Fin /\ B ~<_ ( A X. B ) ) -> B e. Fin )
19 17 18 syldan 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> B e. Fin )
20 10 19 jca 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( A e. Fin /\ B e. Fin ) )