Metamath Proof Explorer

Theorem domssex

Description: Weakening of domssex2 to forget the functions in favor of dominance and equinumerosity. (Contributed by Mario Carneiro, 7-Feb-2015) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion domssex 
|- ( A ~<_ B -> E. x ( A C_ x /\ B ~~ x ) )

Proof

Step Hyp Ref Expression
1 brdomi 
 |-  ( A ~<_ B -> E. f f : A -1-1-> B )
2 reldom 
 |-  Rel ~<_
3 2 brrelex2i 
 |-  ( A ~<_ B -> B e. _V )
4 vex 
 |-  f e. _V
5 f1stres 
 |-  ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) : ( ( B \ ran f ) X. { ~P U. ran A } ) --> ( B \ ran f )
6 difexg 
 |-  ( B e. _V -> ( B \ ran f ) e. _V )
7 6 adantl 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> ( B \ ran f ) e. _V )
8 snex 
 |-  { ~P U. ran A } e. _V
9 xpexg 
 |-  ( ( ( B \ ran f ) e. _V /\ { ~P U. ran A } e. _V ) -> ( ( B \ ran f ) X. { ~P U. ran A } ) e. _V )
10 7 8 9 sylancl 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> ( ( B \ ran f ) X. { ~P U. ran A } ) e. _V )
11 fex2 
 |-  ( ( ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) : ( ( B \ ran f ) X. { ~P U. ran A } ) --> ( B \ ran f ) /\ ( ( B \ ran f ) X. { ~P U. ran A } ) e. _V /\ ( B \ ran f ) e. _V ) -> ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) e. _V )
12 5 10 7 11 mp3an2i 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) e. _V )
13 unexg 
 |-  ( ( f e. _V /\ ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) e. _V ) -> ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) e. _V )
14 4 12 13 sylancr 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) e. _V )
15 cnvexg 
 |-  ( ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) e. _V -> `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) e. _V )
16 14 15 syl 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) e. _V )
17 rnexg 
 |-  ( `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) e. _V -> ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) e. _V )
18 16 17 syl 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) e. _V )
19 simpl 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> f : A -1-1-> B )
20 f1dm 
 |-  ( f : A -1-1-> B -> dom f = A )
21 4 dmex 
 |-  dom f e. _V
22 20 21 eqeltrrdi 
 |-  ( f : A -1-1-> B -> A e. _V )
23 22 adantr 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> A e. _V )
24 simpr 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> B e. _V )
25 eqid 
 |-  `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) = `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) )
26 25 domss2 
 |-  ( ( f : A -1-1-> B /\ A e. _V /\ B e. _V ) -> ( `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) : B -1-1-onto-> ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) /\ A C_ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) /\ ( `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) o. f ) = ( _I |` A ) ) )
27 19 23 24 26 syl3anc 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> ( `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) : B -1-1-onto-> ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) /\ A C_ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) /\ ( `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) o. f ) = ( _I |` A ) ) )
28 27 simp2d 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> A C_ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) )
29 27 simp1d 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) : B -1-1-onto-> ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) )
30 f1oen3g 
 |-  ( ( `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) e. _V /\ `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) : B -1-1-onto-> ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) ) -> B ~~ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) )
31 16 29 30 syl2anc 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> B ~~ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) )
32 28 31 jca 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> ( A C_ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) /\ B ~~ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) ) )
33 sseq2 
 |-  ( x = ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) -> ( A C_ x <-> A C_ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) ) )
34 breq2 
 |-  ( x = ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) -> ( B ~~ x <-> B ~~ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) ) )
35 33 34 anbi12d 
 |-  ( x = ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) -> ( ( A C_ x /\ B ~~ x ) <-> ( A C_ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) /\ B ~~ ran `' ( f u. ( 1st |` ( ( B \ ran f ) X. { ~P U. ran A } ) ) ) ) ) )
36 18 32 35 spcedv 
 |-  ( ( f : A -1-1-> B /\ B e. _V ) -> E. x ( A C_ x /\ B ~~ x ) )
37 36 ex 
 |-  ( f : A -1-1-> B -> ( B e. _V -> E. x ( A C_ x /\ B ~~ x ) ) )
38 37 exlimiv 
 |-  ( E. f f : A -1-1-> B -> ( B e. _V -> E. x ( A C_ x /\ B ~~ x ) ) )
39 1 3 38 sylc 
 |-  ( A ~<_ B -> E. x ( A C_ x /\ B ~~ x ) )