Theorem ssdomg 8932

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 6806	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6774	. . . . . . . . 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 6740	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6672	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 690	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6518	. . . . . . 7 ⊢ Fun I
12		cnvi 6094	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6507	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6563	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6491	. . . . 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 2109  Vcvv 3438   ⊆ wss 3905   class class class wbr 5095   I cid 5517  ^◡ccnv 5622   ↾ cres 5625  Fun wfun 6480  ⟶wf 6482  –1-1→wf1 6483  –onto→wfo 6484  –1-1-onto→wf1o 6485   ≼ cdom 8877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-dom 8881

This theorem is referenced by:  cnvct  8966  xpdom3  8999  domunsncan  9001  domtriord  9047  sdomel  9048  sdomdif  9049  onsdominel  9050  pwdom  9053  2pwuninel  9056  mapdom1  9066  mapdom3  9073  limenpsi  9076  unbnn  9201  nnsdomgOLD  9205  fodomfiOLD  9239  fidomdm  9243  hartogslem1  9453  hartogs  9455  card2on  9465  wdompwdom  9489  wdom2d  9491  wdomima2g  9497  unxpwdom2  9499  unxpwdom  9500  harwdom  9502  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  10485  alephadd  10490  alephmul  10491  alephexp1  10492  alephsuc3  10493  alephexp2  10494  alephreg  10495  pwcfsdom  10496  cfpwsdom  10497  canthnum  10562  pwfseqlem5  10576  pwxpndom2  10578  pwdjundom  10580  gchaleph  10584  gchaleph2  10585  gchac  10594  winainflem  10606  gchina  10612  tsksdom  10669  tskinf  10682  inttsk  10687  inar1  10688  inatsk  10691  tskord  10693  tskcard  10694  grudomon  10730  gruina  10731  axgroth2  10738  axgroth6  10741  grothac  10743  hashun2  14309  hashss  14335  hashsslei  14352  isercoll  15594  o1fsum  15739  incexc2  15764  znnen  16140  qnnen  16141  rpnnen  16155  ruc  16171  phicl2  16698  phibnd  16701  4sqlem11  16886  vdwlem11  16922  0ram  16951  mreexdomd  17574  pgpssslw  19512  fislw  19523  cctop  22910  1stcfb  23349  2ndc1stc  23355  1stcrestlem  23356  2ndcctbss  23359  2ndcdisj2  23361  2ndcsep  23363  dis2ndc  23364  csdfil  23798  ufilen  23834  opnreen  24737  rectbntr0  24738  ovolctb2  25410  uniiccdif  25496  dyadmbl  25518  opnmblALT  25521  vitali  25531  mbfimaopnlem  25573  mbfsup  25582  fta1blem  26093  aannenlem3  26255  ppiwordi  27089  musum  27118  ppiub  27132  chpub  27148  dirith2  27456  upgrex  29056  rabfodom  32468  abrexdomjm  32470  mptctf  32679  locfinreflem  33826  esumcst  34049  omsmeas  34310  sibfof  34327  subfaclefac  35168  erdszelem10  35192  snmlff  35321  finminlem  36311  iccioo01  37320  isinf2  37398  pibt2  37410  phpreu  37603  lindsdom  37613  poimirlem26  37645  mblfinlem1  37656  abrexdom  37729  heiborlem3  37812  ctbnfien  42811  pellexlem4  42825  pellexlem5  42826  ttac  43029  idomodle  43184  idomsubgmo  43186  iscard5  43529  modelaxreplem1  44972  uzct  45061  rn1st  45271  smfaddlem2  46765  smfmullem4  46795  smfpimbor1lem1  46799  aacllem  49806