Theorem ssdomg 5467

Description: A set dominates its subsets. Theorem 16 of [Suppes] p. 94.

Assertion

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

Proof of Theorem ssdomg

Step	Hyp	Ref	Expression
1		f1domg 5455	. 2 |- (A e. C -> (( _I |` A):A-1-1->B -> A ~<_ B))
2		f1oi 4671	. . . . . . . 8 |- ( _I |` A):A-1-1-onto->A
3		dff1o3 4641	. . . . . . . 8 |- (( _I |` A):A-1-1-onto->A <-> (( _I |` A):A-onto->A /\ Fun `'( _I |` A)))
4	2, 3	mpbi 206	. . . . . . 7 |- (( _I |` A):A-onto->A /\ Fun `'( _I |` A))
5	4	simpli 347	. . . . . 6 |- ( _I |` A):A-onto->A
6		fof 4617	. . . . . 6 |- (( _I |` A):A-onto->A -> ( _I |` A):A-->A)
7	5, 6	ax-mp 7	. . . . 5 |- ( _I |` A):A-->A
8		fss 4571	. . . . 5 |- ((( _I |` A):A-->A /\ A C_ B) -> ( _I |` A):A-->B)
9	7, 8	mpan 759	. . . 4 |- (A C_ B -> ( _I |` A):A-->B)
10		funi 4452	. . . . . 6 |- Fun _I
11		cnvi 4320	. . . . . . 7 |- `' _I = _I
12		funeq 4441	. . . . . . 7 |- (`' _I = _I -> (Fun `' _I <-> Fun _I ))
13	11, 12	ax-mp 7	. . . . . 6 |- (Fun `' _I <-> Fun _I )
14	10, 13	mpbir 207	. . . . 5 |- Fun `' _I
15		funres11 4486	. . . . 5 |- (Fun `' _I -> Fun `'( _I |` A))
16	14, 15	ax-mp 7	. . . 4 |- Fun `'( _I |` A)
17	9, 16	jctir 317	. . 3 |- (A C_ B -> (( _I |` A):A-->B /\ Fun `'( _I |` A)))
18		df-f1 4011	. . 3 |- (( _I |` A):A-1-1->B <-> (( _I |` A):A-->B /\ Fun `'( _I |` A)))
19	17, 18	sylibr 217	. 2 |- (A C_ B -> ( _I |` A):A-1-1->B)
20	1, 19	syl5 20	1 |- (A e. C -> (A C_ B -> A ~<_ B))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300   C_ wss 2593   class class class wbr 3338   _I cid 3582  `'ccnv 3985   |` cres 3988  Fun wfun 3992  -->wf 3994  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997   ~<_ cdom 5424

This theorem is referenced by:  ssdom2g 5468  xpdom3 5504  0dom 5527  domtriord 5546  mapdom1 5586  onomeneq 5612  nndomo 5614  omsdomnn 5623  unbnn 5637  pwfilem 5660  hartog 5693  onsdom 5694  omsubsuc2 5878  omsubsdomlem2 5880  omsubel 5883  elomsubsd 5885  omsublim 5887  infenomsub 5889  fodom 5960  carddomi 5986  unxpdomlem 5995  sdomel 5999  ondomon 6008  carduni 6010  cardprc 6013  alephordlem2 6021  alephordi 6022  alephval2 6050  cdadom3 6085  znnen 8771  qnnen 8772  infxpidmlem1 8821  infxpidmlem8 8828  infxpidmlem11 8831  infxpidmlem12 8832  infunabs 8834  infdif 8837  infmap2 8850  alephexp1 8853  axgroth2 10133  axgroth6 10137  sndw 14428  tarax3d2 15225  dmsdtriordOLD 15360  finminlem 15367  fictb 15371  hartogOLD 15384  onsdomOLD 15385  omsubsuc2OLD 15387  omsubsdomlem2OLD 15389  omsubelOLD 15392  elomsubsdOLD 15394  omsublimOLD 15396  infenomsubOLD 15398  2ndc1stc 15477  2ndcctbss 15478  ufilen 15579

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-en 5427  df-dom 5428

Copyright terms: Public domain