Theorem ssdomg 8940

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 5260	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6812	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6780	. . . . . . . . 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 6746	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6678	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 691	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6524	. . . . . . 7 ⊢ Fun I
12		cnvi 6099	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6513	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6569	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6497	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 591	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 480	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8909	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1374	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 413	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890   class class class wbr 5086   I cid 5518  ^◡ccnv 5623   ↾ cres 5626  Fun wfun 6486  ⟶wf 6488  –1-1→wf1 6489  –onto→wfo 6490  –1-1-onto→wf1o 6491   ≼ cdom 8884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-dom 8888

This theorem is referenced by:  cnvct  8974  xpdom3  9006  domunsncan  9008  domtriord  9054  sdomel  9055  sdomdif  9056  onsdominel  9057  pwdom  9060  2pwuninel  9063  mapdom1  9073  mapdom3  9080  limenpsi  9083  unbnn  9199  fodomfiOLD  9233  fidomdm  9237  hartogslem1  9450  hartogs  9452  card2on  9462  wdompwdom  9486  wdom2d  9488  wdomima2g  9494  unxpwdom2  9496  unxpwdom  9497  harwdom  9499  r1sdom  9689  tskwe  9865  carddomi2  9885  cardsdomelir  9888  cardsdomel  9889  harcard  9893  carduni  9896  cardmin2  9914  infxpenlem  9926  ssnum  9952  acnnum  9965  fodomfi2  9973  inffien  9976  alephordi  9987  dfac12lem2  10058  djudoml  10098  cdainflem  10101  djuinf  10102  unctb  10117  infunabs  10119  infdju  10120  infdif  10121  infdif2  10122  infmap2  10130  ackbij2  10155  fictb  10157  cfslb  10179  fincssdom  10236  fin67  10308  fin1a2lem12  10324  axcclem  10370  dmct  10437  brdom3  10441  brdom5  10442  brdom4  10443  imadomg  10447  fnct  10450  mptct  10451  ondomon  10476  alephval2  10486  alephadd  10491  alephmul  10492  alephexp1  10493  alephsuc3  10494  alephexp2  10495  alephreg  10496  pwcfsdom  10497  cfpwsdom  10498  canthnum  10563  pwfseqlem5  10577  pwxpndom2  10579  pwdjundom  10581  gchaleph  10585  gchaleph2  10586  gchac  10595  winainflem  10607  gchina  10613  tsksdom  10670  tskinf  10683  inttsk  10688  inar1  10689  inatsk  10692  tskord  10694  tskcard  10695  grudomon  10731  gruina  10732  axgroth2  10739  axgroth6  10742  grothac  10744  hashun2  14336  hashss  14362  hashsslei  14379  isercoll  15621  o1fsum  15767  incexc2  15794  znnen  16170  qnnen  16171  rpnnen  16185  ruc  16201  phicl2  16729  phibnd  16732  4sqlem11  16917  vdwlem11  16953  0ram  16982  mreexdomd  17606  pgpssslw  19580  fislw  19591  cctop  22981  1stcfb  23420  2ndc1stc  23426  1stcrestlem  23427  2ndcctbss  23430  2ndcdisj2  23432  2ndcsep  23434  dis2ndc  23435  csdfil  23869  ufilen  23905  opnreen  24807  rectbntr0  24808  ovolctb2  25469  uniiccdif  25555  dyadmbl  25577  opnmblALT  25580  vitali  25590  mbfimaopnlem  25632  mbfsup  25641  fta1blem  26146  aannenlem3  26307  ppiwordi  27139  musum  27168  ppiub  27181  chpub  27197  dirith2  27505  upgrex  29175  rabfodom  32590  abrexdomjm  32592  mptctf  32804  locfinreflem  34000  esumcst  34223  omsmeas  34483  sibfof  34500  subfaclefac  35374  erdszelem10  35398  snmlff  35527  finminlem  36516  iccioo01  37657  isinf2  37735  pibt2  37747  phpreu  37939  lindsdom  37949  poimirlem26  37981  mblfinlem1  37992  abrexdom  38065  heiborlem3  38148  ctbnfien  43264  pellexlem4  43278  pellexlem5  43279  ttac  43482  idomodle  43637  idomsubgmo  43639  iscard5  43981  modelaxreplem1  45423  uzct  45512  rn1st  45720  smfaddlem2  47210  smfmullem4  47240  smfpimbor1lem1  47244  aacllem  50288