This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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