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

Metamath Proof Explorer

Theorem ssdomg

Description: A set dominates its subsets. Theorem 16 of Suppes p. 94. (Contributed by NM, 19-Jun-1998) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion ssdomg 
|- ( B e. V -> ( A C_ B -> A ~<_ B ) )

Proof

Step Hyp Ref Expression
1 ssexg 
 |-  ( ( A C_ B /\ B e. V ) -> A e. _V )
2 simpr 
 |-  ( ( A C_ B /\ B e. V ) -> B e. V )
3 f1oi 
 |-  ( _I |` A ) : A -1-1-onto-> A
4 dff1o3 
 |-  ( ( _I |` A ) : A -1-1-onto-> A <-> ( ( _I |` A ) : A -onto-> A /\ Fun `' ( _I |` A ) ) )
5 3 4 mpbi 
 |-  ( ( _I |` A ) : A -onto-> A /\ Fun `' ( _I |` A ) )
6 5 simpli 
 |-  ( _I |` A ) : A -onto-> A
7 fof 
 |-  ( ( _I |` A ) : A -onto-> A -> ( _I |` A ) : A --> A )
8 6 7 ax-mp 
 |-  ( _I |` A ) : A --> A
9 fss 
 |-  ( ( ( _I |` A ) : A --> A /\ A C_ B ) -> ( _I |` A ) : A --> B )
10 8 9 mpan 
 |-  ( A C_ B -> ( _I |` A ) : A --> B )
11 funi 
 |-  Fun _I
12 cnvi 
 |-  `' _I = _I
13 12 funeqi 
 |-  ( Fun `' _I <-> Fun _I )
14 11 13 mpbir 
 |-  Fun `' _I
15 funres11 
 |-  ( Fun `' _I -> Fun `' ( _I |` A ) )
16 14 15 ax-mp 
 |-  Fun `' ( _I |` A )
17 df-f1 
 |-  ( ( _I |` A ) : A -1-1-> B <-> ( ( _I |` A ) : A --> B /\ Fun `' ( _I |` A ) ) )
18 10 16 17 sylanblrc 
 |-  ( A C_ B -> ( _I |` A ) : A -1-1-> B )
19 18 adantr 
 |-  ( ( A C_ B /\ B e. V ) -> ( _I |` A ) : A -1-1-> B )
20 f1dom2g 
 |-  ( ( A e. _V /\ B e. V /\ ( _I |` A ) : A -1-1-> B ) -> A ~<_ B )
21 1 2 19 20 syl3anc 
 |-  ( ( A C_ B /\ B e. V ) -> A ~<_ B )
22 21 expcom 
 |-  ( B e. V -> ( A C_ B -> A ~<_ B ) )