Theorem ssdomg 9012

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

Assertion

Ref	Expression
ssdomg	⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Proof of Theorem ssdomg

Step	Hyp	Ref	Expression
1		ssexg 5293	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6855	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6823	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 230	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 483	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6789	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6721	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 690	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6567	. . . . . . 7 ⊢ Fun I
12		cnvi 6130	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6556	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6612	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6535	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 590	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 480	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8982	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1373	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 413	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Vcvv 3459   ⊆ wss 3926   class class class wbr 5119   I cid 5547  ^◡ccnv 5653   ↾ cres 5656  Fun wfun 6524  ⟶wf 6526  –1-1→wf1 6527  –onto→wfo 6528  –1-1-onto→wf1o 6529   ≼ cdom 8955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-dom 8959

This theorem is referenced by:  cnvct  9046  ssctOLD  9064  undomOLD  9072  xpdom3  9082  domunsncan  9084  sucdom2OLD  9094  0domgOLD  9113  domtriord  9135  sdomel  9136  sdomdif  9137  onsdominel  9138  pwdom  9141  2pwuninel  9144  mapdom1  9154  mapdom3  9161  limenpsi  9164  phpOLD  9229  php2OLD  9230  php3OLD  9231  nndomogOLD  9233  onomeneqOLD  9236  unbnn  9302  nnsdomgOLD  9306  fodomfiOLD  9340  fidomdm  9344  hartogslem1  9554  hartogs  9556  card2on  9566  wdompwdom  9590  wdom2d  9592  wdomima2g  9598  unxpwdom2  9600  unxpwdom  9601  harwdom  9603  r1sdom  9786  tskwe  9962  carddomi2  9982  cardsdomelir  9985  cardsdomel  9986  harcard  9990  carduni  9993  cardmin2  10011  infxpenlem  10025  ssnum  10051  acnnum  10064  fodomfi2  10072  inffien  10075  alephordi  10086  dfac12lem2  10157  djudoml  10197  cdainflem  10200  djuinf  10201  unctb  10216  infunabs  10218  infdju  10219  infdif  10220  infdif2  10221  infmap2  10229  ackbij2  10254  fictb  10256  cfslb  10278  fincssdom  10335  fin67  10407  fin1a2lem12  10423  axcclem  10469  dmct  10536  brdom3  10540  brdom5  10541  brdom4  10542  imadomg  10546  fnct  10549  mptct  10550  ondomon  10575  alephval2  10584  alephadd  10589  alephmul  10590  alephexp1  10591  alephsuc3  10592  alephexp2  10593  alephreg  10594  pwcfsdom  10595  cfpwsdom  10596  canthnum  10661  pwfseqlem5  10675  pwxpndom2  10677  pwdjundom  10679  gchaleph  10683  gchaleph2  10684  gchac  10693  winainflem  10705  gchina  10711  tsksdom  10768  tskinf  10781  inttsk  10786  inar1  10787  inatsk  10790  tskord  10792  tskcard  10793  grudomon  10829  gruina  10830  axgroth2  10837  axgroth6  10840  grothac  10842  hashun2  14399  hashss  14425  hashsslei  14442  isercoll  15682  o1fsum  15827  incexc2  15852  znnen  16228  qnnen  16229  rpnnen  16243  ruc  16259  phicl2  16785  phibnd  16788  4sqlem11  16973  vdwlem11  17009  0ram  17038  mreexdomd  17659  pgpssslw  19593  fislw  19604  cctop  22942  1stcfb  23381  2ndc1stc  23387  1stcrestlem  23388  2ndcctbss  23391  2ndcdisj2  23393  2ndcsep  23395  dis2ndc  23396  csdfil  23830  ufilen  23866  opnreen  24769  rectbntr0  24770  ovolctb2  25443  uniiccdif  25529  dyadmbl  25551  opnmblALT  25554  vitali  25564  mbfimaopnlem  25606  mbfsup  25615  fta1blem  26126  aannenlem3  26288  ppiwordi  27122  musum  27151  ppiub  27165  chpub  27181  dirith2  27489  upgrex  29017  rabfodom  32432  abrexdomjm  32434  mptctf  32641  locfinreflem  33817  esumcst  34040  omsmeas  34301  sibfof  34318  subfaclefac  35144  erdszelem10  35168  snmlff  35297  finminlem  36282  iccioo01  37291  isinf2  37369  pibt2  37381  phpreu  37574  lindsdom  37584  poimirlem26  37616  mblfinlem1  37627  abrexdom  37700  heiborlem3  37783  ctbnfien  42788  pellexlem4  42802  pellexlem5  42803  ttac  43007  idomodle  43162  idomsubgmo  43164  iscard5  43507  modelaxreplem1  44951  uzct  45035  rn1st  45245  smfaddlem2  46741  smfmullem4  46771  smfpimbor1lem1  46775  aacllem  49613