Theorem ssdomg 7887

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 4732	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 476	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6086	. . . . . . . . . 10 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6056	. . . . . . . . . 10 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 219	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 473	. . . . . . . 8 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6028	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 5969	. . . . . . 7 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 702	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 5834	. . . . . . . 8 ⊢ Fun I
12		cnvi 5456	. . . . . . . . 9 ⊢ ◡ I = I
13	12	funeqi 5824	. . . . . . . 8 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 220	. . . . . . 7 ⊢ Fun ◡ I
15		funres11 5880	. . . . . . 7 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . . 6 ⊢ Fun ◡( I ↾ 𝐴)
17	10, 16	jctir 559	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18		df-f1 5809	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
19	17, 18	sylibr 223	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20	19	adantr 480	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
21		f1dom2g 7859	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
22	1, 2, 20, 21	syl3anc 1318	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
23	22	expcom 450	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540   class class class wbr 4583   I cid 4948  ^◡ccnv 5037   ↾ cres 5040  Fun wfun 5798  ⟶wf 5800  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803   ≼ cdom 7839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-dom 7843

This theorem is referenced by:  ssct  7926  undom  7933  xpdom3  7943  domunsncan  7945  0domg  7972  domtriord  7991  sdomel  7992  sdomdif  7993  onsdominel  7994  pwdom  7997  2pwuninel  8000  mapdom1  8010  mapdom3  8017  limenpsi  8020  php  8029  php2  8030  php3  8031  onomeneq  8035  nndomo  8039  sucdom2  8041  unbnn  8101  nnsdomg  8104  fodomfi  8124  fidomdm  8128  pwfilem  8143  hartogslem1  8330  hartogs  8332  card2on  8342  wdompwdom  8366  wdom2d  8368  wdomima2g  8374  unxpwdom2  8376  unxpwdom  8377  harwdom  8378  r1sdom  8520  tskwe  8659  carddomi2  8679  cardsdomelir  8682  cardsdomel  8683  harcard  8687  carduni  8690  cardmin2  8707  infxpenlem  8719  ssnum  8745  acnnum  8758  fodomfi2  8766  inffien  8769  alephordi  8780  dfac12lem2  8849  cdadom3  8893  cdainflem  8896  cdainf  8897  unctb  8910  infunabs  8912  infcda  8913  infdif  8914  infdif2  8915  infmap2  8923  ackbij2  8948  fictb  8950  cfslb  8971  fincssdom  9028  fin67  9100  fin1a2lem12  9116  axcclem  9162  brdom3  9231  brdom5  9232  brdom4  9233  imadomg  9237  ondomon  9264  alephval2  9273  alephadd  9278  alephmul  9279  alephexp1  9280  alephsuc3  9281  alephexp2  9282  alephreg  9283  pwcfsdom  9284  cfpwsdom  9285  canthnum  9350  pwfseqlem5  9364  pwxpndom2  9366  pwcdandom  9368  gchaleph  9372  gchaleph2  9373  gchac  9382  winainflem  9394  gchina  9400  tsksdom  9457  tskinf  9470  inttsk  9475  inar1  9476  inatsk  9479  tskord  9481  tskcard  9482  grudomon  9518  gruina  9519  axgroth2  9526  axgroth6  9529  grothac  9531  hashun2  13033  hashss  13058  hashsslei  13073  isercoll  14246  o1fsum  14386  incexc2  14409  znnen  14780  qnnen  14781  rpnnen  14795  ruc  14811  phicl2  15311  phibnd  15314  4sqlem11  15497  vdwlem11  15533  0ram  15562  mreexdomd  16133  pgpssslw  17852  fislw  17863  cctop  20620  1stcfb  21058  2ndc1stc  21064  1stcrestlem  21065  2ndcctbss  21068  2ndcdisj2  21070  2ndcsep  21072  dis2ndc  21073  csdfil  21508  ufilen  21544  opnreen  22442  rectbntr0  22443  ovolctb2  23067  uniiccdif  23152  dyadmbl  23174  opnmblALT  23177  vitali  23188  mbfimaopnlem  23228  mbfsup  23237  fta1blem  23732  aannenlem3  23889  ppiwordi  24688  musum  24717  ppiub  24729  chpub  24745  dchrisum0re  25002  dirith2  25017  upgrex  25759  umgraex  25852  konigsberg  26514  rabfodom  28728  abrexdomjm  28729  fnct  28876  dmct  28877  cnvct  28878  mptct  28880  mptctf  28883  locfinreflem  29235  esumcst  29452  omsmeas  29712  sibfof  29729  subfaclefac  30412  erdszelem10  30436  snmlff  30565  finminlem  31482  phpreu  32563  lindsdom  32573  poimirlem26  32605  mblfinlem1  32616  abrexdom  32695  heiborlem3  32782  ctbnfien  36400  pellexlem4  36414  pellexlem5  36415  ttac  36621  idomodle  36793  idomsubgmo  36795  uzct  38257  smfaddlem2  39650  smfmullem4  39679  smfpimbor1lem1  39683  aacllem  42356