Theorem ssdomg 8287

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 5041	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 479	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6428	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6397	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 222	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 478	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6366	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6304	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 680	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6167	. . . . . . 7 ⊢ Fun I
12		cnvi 5791	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6156	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 223	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6211	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6140	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 584	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 474	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8259	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1439	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 404	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107  Vcvv 3398   ⊆ wss 3792   class class class wbr 4886   I cid 5260  ^◡ccnv 5354   ↾ cres 5357  Fun wfun 6129  ⟶wf 6131  –1-1→wf1 6132  –onto→wfo 6133  –1-1-onto→wf1o 6134   ≼ cdom 8239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-dom 8243

This theorem is referenced by:  cnvct  8318  ssct  8329  undom  8336  xpdom3  8346  domunsncan  8348  0domg  8375  domtriord  8394  sdomel  8395  sdomdif  8396  onsdominel  8397  pwdom  8400  2pwuninel  8403  mapdom1  8413  mapdom3  8420  limenpsi  8423  php  8432  php2  8433  php3  8434  onomeneq  8438  nndomo  8442  sucdom2  8444  unbnn  8504  nnsdomg  8507  fodomfi  8527  fidomdm  8531  pwfilem  8548  hartogslem1  8736  hartogs  8738  card2on  8748  wdompwdom  8772  wdom2d  8774  wdomima2g  8780  unxpwdom2  8782  unxpwdom  8783  harwdom  8784  r1sdom  8934  tskwe  9109  carddomi2  9129  cardsdomelir  9132  cardsdomel  9133  harcard  9137  carduni  9140  cardmin2  9157  infxpenlem  9169  ssnum  9195  acnnum  9208  fodomfi2  9216  inffien  9219  alephordi  9230  dfac12lem2  9301  cdadom3  9345  cdainflem  9348  cdainf  9349  unctb  9362  infunabs  9364  infcda  9365  infdif  9366  infdif2  9367  infmap2  9375  ackbij2  9400  fictb  9402  cfslb  9423  fincssdom  9480  fin67  9552  fin1a2lem12  9568  axcclem  9614  dmct  9681  brdom3  9685  brdom5  9686  brdom4  9687  imadomg  9691  fnct  9694  mptct  9695  ondomon  9720  alephval2  9729  alephadd  9734  alephmul  9735  alephexp1  9736  alephsuc3  9737  alephexp2  9738  alephreg  9739  pwcfsdom  9740  cfpwsdom  9741  canthnum  9806  pwfseqlem5  9820  pwxpndom2  9822  pwcdandom  9824  gchaleph  9828  gchaleph2  9829  gchac  9838  winainflem  9850  gchina  9856  tsksdom  9913  tskinf  9926  inttsk  9931  inar1  9932  inatsk  9935  tskord  9937  tskcard  9938  grudomon  9974  gruina  9975  axgroth2  9982  axgroth6  9985  grothac  9987  hashun2  13487  hashss  13511  hashsslei  13527  isercoll  14806  o1fsum  14949  incexc2  14974  znnen  15345  qnnen  15346  rpnnen  15360  ruc  15376  phicl2  15877  phibnd  15880  4sqlem11  16063  vdwlem11  16099  0ram  16128  mreexdomd  16695  pgpssslw  18413  fislw  18424  cctop  21218  1stcfb  21657  2ndc1stc  21663  1stcrestlem  21664  2ndcctbss  21667  2ndcdisj2  21669  2ndcsep  21671  dis2ndc  21672  csdfil  22106  ufilen  22142  opnreen  23042  rectbntr0  23043  ovolctb2  23696  uniiccdif  23782  dyadmbl  23804  opnmblALT  23807  vitali  23817  mbfimaopnlem  23859  mbfsup  23868  fta1blem  24365  aannenlem3  24522  ppiwordi  25340  musum  25369  ppiub  25381  chpub  25397  dchrisum0re  25654  dirith2  25669  upgrex  26440  rabfodom  29906  abrexdomjm  29907  mptctf  30061  locfinreflem  30505  esumcst  30723  omsmeas  30983  sibfof  31000  subfaclefac  31757  erdszelem10  31781  snmlff  31910  finminlem  32901  phpreu  34020  lindsdom  34031  poimirlem26  34063  mblfinlem1  34074  abrexdom  34152  heiborlem3  34238  ctbnfien  38346  pellexlem4  38360  pellexlem5  38361  ttac  38566  idomodle  38737  idomsubgmo  38739  uzct  40167  smfaddlem2  41903  smfmullem4  41932  smfpimbor1lem1  41936  aacllem  43657