Metamath Proof Explorer

Theorem sucxpdom

Description: Cartesian product dominates successor for set with cardinality greater than 1. Proposition 10.38 of TakeutiZaring p. 93 (but generalized to arbitrary sets, not just ordinals). (Contributed by NM, 3-Sep-2004) (Proof shortened by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion sucxpdom 
|- ( 1o ~< A -> suc A ~<_ ( A X. A ) )

Proof

Step Hyp Ref Expression
1 df-suc 
 |-  suc A = ( A u. { A } )
2 relsdom 
 |-  Rel ~<
3 2 brrelex2i 
 |-  ( 1o ~< A -> A e. _V )
4 1on 
 |-  1o e. On
5 xpsneng 
 |-  ( ( A e. _V /\ 1o e. On ) -> ( A X. { 1o } ) ~~ A )
6 3 4 5 sylancl 
 |-  ( 1o ~< A -> ( A X. { 1o } ) ~~ A )
7 6 ensymd 
 |-  ( 1o ~< A -> A ~~ ( A X. { 1o } ) )
8 endom 
 |-  ( A ~~ ( A X. { 1o } ) -> A ~<_ ( A X. { 1o } ) )
9 7 8 syl 
 |-  ( 1o ~< A -> A ~<_ ( A X. { 1o } ) )
10 ensn1g 
 |-  ( A e. _V -> { A } ~~ 1o )
11 3 10 syl 
 |-  ( 1o ~< A -> { A } ~~ 1o )
12 ensdomtr 
 |-  ( ( { A } ~~ 1o /\ 1o ~< A ) -> { A } ~< A )
13 11 12 mpancom 
 |-  ( 1o ~< A -> { A } ~< A )
14 0ex 
 |-  (/) e. _V
15 xpsneng 
 |-  ( ( A e. _V /\ (/) e. _V ) -> ( A X. { (/) } ) ~~ A )
16 3 14 15 sylancl 
 |-  ( 1o ~< A -> ( A X. { (/) } ) ~~ A )
17 16 ensymd 
 |-  ( 1o ~< A -> A ~~ ( A X. { (/) } ) )
18 sdomentr 
 |-  ( ( { A } ~< A /\ A ~~ ( A X. { (/) } ) ) -> { A } ~< ( A X. { (/) } ) )
19 13 17 18 syl2anc 
 |-  ( 1o ~< A -> { A } ~< ( A X. { (/) } ) )
20 sdomdom 
 |-  ( { A } ~< ( A X. { (/) } ) -> { A } ~<_ ( A X. { (/) } ) )
21 19 20 syl 
 |-  ( 1o ~< A -> { A } ~<_ ( A X. { (/) } ) )
22 1n0 
 |-  1o =/= (/)
23 xpsndisj 
 |-  ( 1o =/= (/) -> ( ( A X. { 1o } ) i^i ( A X. { (/) } ) ) = (/) )
24 22 23 mp1i 
 |-  ( 1o ~< A -> ( ( A X. { 1o } ) i^i ( A X. { (/) } ) ) = (/) )
25 undom 
 |-  ( ( ( A ~<_ ( A X. { 1o } ) /\ { A } ~<_ ( A X. { (/) } ) ) /\ ( ( A X. { 1o } ) i^i ( A X. { (/) } ) ) = (/) ) -> ( A u. { A } ) ~<_ ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) )
26 9 21 24 25 syl21anc 
 |-  ( 1o ~< A -> ( A u. { A } ) ~<_ ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) )
27 sdomentr 
 |-  ( ( 1o ~< A /\ A ~~ ( A X. { 1o } ) ) -> 1o ~< ( A X. { 1o } ) )
28 7 27 mpdan 
 |-  ( 1o ~< A -> 1o ~< ( A X. { 1o } ) )
29 sdomentr 
 |-  ( ( 1o ~< A /\ A ~~ ( A X. { (/) } ) ) -> 1o ~< ( A X. { (/) } ) )
30 17 29 mpdan 
 |-  ( 1o ~< A -> 1o ~< ( A X. { (/) } ) )
31 unxpdom 
 |-  ( ( 1o ~< ( A X. { 1o } ) /\ 1o ~< ( A X. { (/) } ) ) -> ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) ~<_ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) )
32 28 30 31 syl2anc 
 |-  ( 1o ~< A -> ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) ~<_ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) )
33 domtr 
 |-  ( ( ( A u. { A } ) ~<_ ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) /\ ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) ~<_ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) ) -> ( A u. { A } ) ~<_ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) )
34 26 32 33 syl2anc 
 |-  ( 1o ~< A -> ( A u. { A } ) ~<_ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) )
35 xpen 
 |-  ( ( ( A X. { 1o } ) ~~ A /\ ( A X. { (/) } ) ~~ A ) -> ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) ~~ ( A X. A ) )
36 6 16 35 syl2anc 
 |-  ( 1o ~< A -> ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) ~~ ( A X. A ) )
37 domentr 
 |-  ( ( ( A u. { A } ) ~<_ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) /\ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) ~~ ( A X. A ) ) -> ( A u. { A } ) ~<_ ( A X. A ) )
38 34 36 37 syl2anc 
 |-  ( 1o ~< A -> ( A u. { A } ) ~<_ ( A X. A ) )
39 1 38 eqbrtrid 
 |-  ( 1o ~< A -> suc A ~<_ ( A X. A ) )