Theorem ssdomg 8933

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 5265	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6809	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6777	. . . . . . . . 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 6743	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6675	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 690	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6521	. . . . . . 7 ⊢ Fun I
12		cnvi 6096	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6510	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6566	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6494	. . . . 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 8902	. . 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 2113  Vcvv 3437   ⊆ wss 3898   class class class wbr 5095   I cid 5515  ^◡ccnv 5620   ↾ cres 5623  Fun wfun 6483  ⟶wf 6485  –1-1→wf1 6486  –onto→wfo 6487  –1-1-onto→wf1o 6488   ≼ cdom 8877

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 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677

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-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-dom 8881

This theorem is referenced by:  cnvct  8967  xpdom3  8999  domunsncan  9001  domtriord  9047  sdomel  9048  sdomdif  9049  onsdominel  9050  pwdom  9053  2pwuninel  9056  mapdom1  9066  mapdom3  9073  limenpsi  9076  unbnn  9191  fodomfiOLD  9225  fidomdm  9229  hartogslem1  9439  hartogs  9441  card2on  9451  wdompwdom  9475  wdom2d  9477  wdomima2g  9483  unxpwdom2  9485  unxpwdom  9486  harwdom  9488  r1sdom  9678  tskwe  9854  carddomi2  9874  cardsdomelir  9877  cardsdomel  9878  harcard  9882  carduni  9885  cardmin2  9903  infxpenlem  9915  ssnum  9941  acnnum  9954  fodomfi2  9962  inffien  9965  alephordi  9976  dfac12lem2  10047  djudoml  10087  cdainflem  10090  djuinf  10091  unctb  10106  infunabs  10108  infdju  10109  infdif  10110  infdif2  10111  infmap2  10119  ackbij2  10144  fictb  10146  cfslb  10168  fincssdom  10225  fin67  10297  fin1a2lem12  10313  axcclem  10359  dmct  10426  brdom3  10430  brdom5  10431  brdom4  10432  imadomg  10436  fnct  10439  mptct  10440  ondomon  10465  alephval2  10474  alephadd  10479  alephmul  10480  alephexp1  10481  alephsuc3  10482  alephexp2  10483  alephreg  10484  pwcfsdom  10485  cfpwsdom  10486  canthnum  10551  pwfseqlem5  10565  pwxpndom2  10567  pwdjundom  10569  gchaleph  10573  gchaleph2  10574  gchac  10583  winainflem  10595  gchina  10601  tsksdom  10658  tskinf  10671  inttsk  10676  inar1  10677  inatsk  10680  tskord  10682  tskcard  10683  grudomon  10719  gruina  10720  axgroth2  10727  axgroth6  10730  grothac  10732  hashun2  14297  hashss  14323  hashsslei  14340  isercoll  15582  o1fsum  15727  incexc2  15752  znnen  16128  qnnen  16129  rpnnen  16143  ruc  16159  phicl2  16686  phibnd  16689  4sqlem11  16874  vdwlem11  16910  0ram  16939  mreexdomd  17563  pgpssslw  19534  fislw  19545  cctop  22941  1stcfb  23380  2ndc1stc  23386  1stcrestlem  23387  2ndcctbss  23390  2ndcdisj2  23392  2ndcsep  23394  dis2ndc  23395  csdfil  23829  ufilen  23865  opnreen  24767  rectbntr0  24768  ovolctb2  25440  uniiccdif  25526  dyadmbl  25548  opnmblALT  25551  vitali  25561  mbfimaopnlem  25603  mbfsup  25612  fta1blem  26123  aannenlem3  26285  ppiwordi  27119  musum  27148  ppiub  27162  chpub  27178  dirith2  27486  upgrex  29091  rabfodom  32506  abrexdomjm  32508  mptctf  32723  locfinreflem  33925  esumcst  34148  omsmeas  34408  sibfof  34425  subfaclefac  35292  erdszelem10  35316  snmlff  35445  finminlem  36434  iccioo01  37444  isinf2  37522  pibt2  37534  phpreu  37717  lindsdom  37727  poimirlem26  37759  mblfinlem1  37770  abrexdom  37843  heiborlem3  37926  ctbnfien  42975  pellexlem4  42989  pellexlem5  42990  ttac  43193  idomodle  43348  idomsubgmo  43350  iscard5  43693  modelaxreplem1  45135  uzct  45224  rn1st  45433  smfaddlem2  46924  smfmullem4  46954  smfpimbor1lem1  46958  aacllem  49962