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