Theorem xpdom3

Description: A set is dominated by its Cartesian product with a nonempty set. Exercise 6 of Suppes p. 98. (Contributed by NM, 27-Jul-2004) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	xpdom3	|- ( ( A e. V /\ B e. W /\ B =/= (/) ) -> A ~<_ ( A X. B ) )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( B =/= (/) <-> E. x x e. B )
2		xpsneng	|- ( ( A e. V /\ x e. B ) -> ( A X. { x } ) ~~ A )
3	2	3adant2	|- ( ( A e. V /\ B e. W /\ x e. B ) -> ( A X. { x } ) ~~ A )
4	3	ensymd	|- ( ( A e. V /\ B e. W /\ x e. B ) -> A ~~ ( A X. { x } ) )
5		xpexg	|- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
6	5	3adant3	|- ( ( A e. V /\ B e. W /\ x e. B ) -> ( A X. B ) e. _V )
7		simp3	|- ( ( A e. V /\ B e. W /\ x e. B ) -> x e. B )
8	7	snssd	|- ( ( A e. V /\ B e. W /\ x e. B ) -> { x } C_ B )
9		xpss2	|- ( { x } C_ B -> ( A X. { x } ) C_ ( A X. B ) )
10	8 9	syl	|- ( ( A e. V /\ B e. W /\ x e. B ) -> ( A X. { x } ) C_ ( A X. B ) )
11		ssdomg	|- ( ( A X. B ) e. _V -> ( ( A X. { x } ) C_ ( A X. B ) -> ( A X. { x } ) ~<_ ( A X. B ) ) )
12	6 10 11	sylc	|- ( ( A e. V /\ B e. W /\ x e. B ) -> ( A X. { x } ) ~<_ ( A X. B ) )
13		endomtr	|- ( ( A ~~ ( A X. { x } ) /\ ( A X. { x } ) ~<_ ( A X. B ) ) -> A ~<_ ( A X. B ) )
14	4 12 13	syl2anc	|- ( ( A e. V /\ B e. W /\ x e. B ) -> A ~<_ ( A X. B ) )
15	14	3expia	|- ( ( A e. V /\ B e. W ) -> ( x e. B -> A ~<_ ( A X. B ) ) )
16	15	exlimdv	|- ( ( A e. V /\ B e. W ) -> ( E. x x e. B -> A ~<_ ( A X. B ) ) )
17	1 16	biimtrid	|- ( ( A e. V /\ B e. W ) -> ( B =/= (/) -> A ~<_ ( A X. B ) ) )
18	17	3impia	|- ( ( A e. V /\ B e. W /\ B =/= (/) ) -> A ~<_ ( A X. B ) )