Theorem ssdomg 8937

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 5251	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 485	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6805	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6773	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 231	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 484	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6739	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6671	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 696	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6517	. . . . . . 7 ⊢ Fun I
12		cnvi 6092	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6506	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 232	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6562	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6490	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 596	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 481	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8906	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1379	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 414	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  Vcvv 3431   ⊆ wss 3883   class class class wbr 5072   I cid 5512  ^◡ccnv 5617   ↾ cres 5620  Fun wfun 6479  ⟶wf 6481  –1-1→wf1 6482  –onto→wfo 6483  –1-1-onto→wf1o 6484   ≼ cdom 8881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-dom 8885

This theorem is referenced by:  cnvct  8971  xpdom3  9003  domunsncan  9005  domtriord  9051  sdomel  9052  sdomdif  9053  onsdominel  9054  pwdom  9057  2pwuninel  9060  mapdom1  9070  mapdom3  9077  limenpsi  9080  unbnn  9196  fodomfiOLD  9230  fidomdm  9234  hartogslem1  9447  hartogs  9449  card2on  9459  wdompwdom  9483  wdom2d  9485  wdomima2g  9491  unxpwdom2  9493  unxpwdom  9494  harwdom  9496  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  22989  1stcfb  23428  2ndc1stc  23434  1stcrestlem  23435  2ndcctbss  23438  2ndcdisj2  23440  2ndcsep  23442  dis2ndc  23443  csdfil  23877  ufilen  23913  opnreen  24815  rectbntr0  24816  ovolctb2  25477  uniiccdif  25563  dyadmbl  25585  opnmblALT  25588  vitali  25598  mbfimaopnlem  25640  mbfsup  25649  fta1blem  26154  aannenlem3  26314  ppiwordi  27143  musum  27172  ppiub  27185  chpub  27201  dirith2  27509  upgrex  29179  rabfodom  32593  abrexdomjm  32595  mptctf  32808  locfinreflem  34024  esumcst  34247  omsmeas  34507  sibfof  34524  subfaclefac  35404  erdszelem10  35428  snmlff  35557  finminlem  36546  iccioo01  37689  isinf2  37767  pibt2  37779  phpreu  37971  lindsdom  37981  poimirlem26  38013  mblfinlem1  38024  abrexdom  38097  heiborlem3  38180  ctbnfien  43263  pellexlem4  43277  pellexlem5  43278  ttac  43481  idomodle  43636  idomsubgmo  43638  iscard5  43980  modelaxreplem1  45422  uzct  45511  rn1st  45717  smfaddlem2  47207  smfmullem4  47237  smfpimbor1lem1  47241  aacllem  50291