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