Theorem ssdomg 8917

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 5256	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6796	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6764	. . . . . . . . 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 6730	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6662	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 690	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6508	. . . . . . 7 ⊢ Fun I
12		cnvi 6083	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6497	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6553	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6481	. . . . 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 8887	. . 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 2111  Vcvv 3436   ⊆ wss 3897   class class class wbr 5086   I cid 5505  ^◡ccnv 5610   ↾ cres 5613  Fun wfun 6470  ⟶wf 6472  –1-1→wf1 6473  –onto→wfo 6474  –1-1-onto→wf1o 6475   ≼ cdom 8862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-dom 8866

This theorem is referenced by:  cnvct  8951  xpdom3  8983  domunsncan  8985  domtriord  9031  sdomel  9032  sdomdif  9033  onsdominel  9034  pwdom  9037  2pwuninel  9040  mapdom1  9050  mapdom3  9057  limenpsi  9060  unbnn  9175  fodomfiOLD  9209  fidomdm  9213  hartogslem1  9423  hartogs  9425  card2on  9435  wdompwdom  9459  wdom2d  9461  wdomima2g  9467  unxpwdom2  9469  unxpwdom  9470  harwdom  9472  r1sdom  9662  tskwe  9838  carddomi2  9858  cardsdomelir  9861  cardsdomel  9862  harcard  9866  carduni  9869  cardmin2  9887  infxpenlem  9899  ssnum  9925  acnnum  9938  fodomfi2  9946  inffien  9949  alephordi  9960  dfac12lem2  10031  djudoml  10071  cdainflem  10074  djuinf  10075  unctb  10090  infunabs  10092  infdju  10093  infdif  10094  infdif2  10095  infmap2  10103  ackbij2  10128  fictb  10130  cfslb  10152  fincssdom  10209  fin67  10281  fin1a2lem12  10297  axcclem  10343  dmct  10410  brdom3  10414  brdom5  10415  brdom4  10416  imadomg  10420  fnct  10423  mptct  10424  ondomon  10449  alephval2  10458  alephadd  10463  alephmul  10464  alephexp1  10465  alephsuc3  10466  alephexp2  10467  alephreg  10468  pwcfsdom  10469  cfpwsdom  10470  canthnum  10535  pwfseqlem5  10549  pwxpndom2  10551  pwdjundom  10553  gchaleph  10557  gchaleph2  10558  gchac  10567  winainflem  10579  gchina  10585  tsksdom  10642  tskinf  10655  inttsk  10660  inar1  10661  inatsk  10664  tskord  10666  tskcard  10667  grudomon  10703  gruina  10704  axgroth2  10711  axgroth6  10714  grothac  10716  hashun2  14285  hashss  14311  hashsslei  14328  isercoll  15570  o1fsum  15715  incexc2  15740  znnen  16116  qnnen  16117  rpnnen  16131  ruc  16147  phicl2  16674  phibnd  16677  4sqlem11  16862  vdwlem11  16898  0ram  16927  mreexdomd  17550  pgpssslw  19521  fislw  19532  cctop  22916  1stcfb  23355  2ndc1stc  23361  1stcrestlem  23362  2ndcctbss  23365  2ndcdisj2  23367  2ndcsep  23369  dis2ndc  23370  csdfil  23804  ufilen  23840  opnreen  24742  rectbntr0  24743  ovolctb2  25415  uniiccdif  25501  dyadmbl  25523  opnmblALT  25526  vitali  25536  mbfimaopnlem  25578  mbfsup  25587  fta1blem  26098  aannenlem3  26260  ppiwordi  27094  musum  27123  ppiub  27137  chpub  27153  dirith2  27461  upgrex  29065  rabfodom  32477  abrexdomjm  32479  mptctf  32691  locfinreflem  33845  esumcst  34068  omsmeas  34328  sibfof  34345  subfaclefac  35212  erdszelem10  35236  snmlff  35365  finminlem  36352  iccioo01  37361  isinf2  37439  pibt2  37451  phpreu  37644  lindsdom  37654  poimirlem26  37686  mblfinlem1  37697  abrexdom  37770  heiborlem3  37853  ctbnfien  42851  pellexlem4  42865  pellexlem5  42866  ttac  43069  idomodle  43224  idomsubgmo  43226  iscard5  43569  modelaxreplem1  45011  uzct  45100  rn1st  45310  smfaddlem2  46802  smfmullem4  46832  smfpimbor1lem1  46836  aacllem  49833