Theorem ssdomg 9065

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 5288	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 490	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6894	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴⟶1-1onto𝐴
4		dff1o3 6861	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴⟶1-1onto𝐴 ↔ (( I ↾ 𝐴):𝐴⟶onto𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 233	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴⟶onto𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 489	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴⟶onto𝐴
7		fof 6826	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴⟶onto𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6756	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 703	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6600	. . . . . . 7 ⊢ Fun I
12		cnvi 5875	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6588	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 234	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6647	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6571	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴⟶1-1𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 602	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶1-1𝐵)
19	18	adantr 486	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴⟶1-1𝐵)
20		f1dom2g 9034	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴⟶1-1𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1399	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 419	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   class class class wbr 5108   I cid 5552  ^◡ccnv 5657   ↾ cres 5660  Fun wfun 6560  ⟶wf 6562  ⟶1-1wf1 6563  ⟶ontowfo 6564  ⟶1-1ontowf1o 6565   ≼ cdom 9009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-dom 9013

This theorem is used by:  cnvct  9100  xpdom3  9132  domunsncan  9134  domtriord  9180  sdomel  9181  sdomdif  9182  onsdominel  9183  pwdom  9186  2pwuninel  9189  mapdom1  9199  mapdom3  9206  limenpsi  9209  unbnn  9326  fidomdm  9361  hartogslem1  9573  hartogs  9575  card2on  9585  wdompwdom  9609  wdom2d  9611  wdomima2g  9617  unxpwdom2  9619  unxpwdom  9620  harwdom  9622  r1sdom  9818  tskwe  10068  carddomi2  10088  cardsdomelir  10091  cardsdomel  10092  harcard  10096  cardprcr  10099  carduni  10101  cardmin2  10119  infxpenlem  10131  ssnum  10157  acnnum  10170  fodomfi2  10178  inffien  10181  alephordi  10192  dfac12lem2  10262  djudoml  10302  cdainflem  10305  djuinf  10306  unctb  10321  infunabs  10323  infdju  10324  infdif  10325  infdif2  10326  infmap2  10334  ackbij2  10359  fictb  10361  cfslb  10383  fincssdom  10440  fin67  10512  fin1a2lem12  10528  axcclem  10574  dmct  10641  dmctOLD  10642  brdom3  10646  brdom5  10647  brdom4  10648  imadomg  10652  imadomnum  10653  fnct  10659  fnctOLD  10660  mptct  10661  ondomon  10686  alephval2  10696  alephadd  10701  alephmul  10702  alephexp1  10703  alephsuc3  10704  alephexp2  10705  alephreg  10706  pwcfsdom  10707  cfpwsdom  10708  canthnum  10773  pwfseqlem5  10787  pwxpndom2  10789  pwdjundom  10791  gchaleph  10795  gchaleph2  10796  gchac  10805  winainflem  10817  gchina  10823  tsksdom  10880  tskinf  10893  inttsk  10898  inar1  10899  inatsk  10902  tskord  10904  tskcard  10905  grudomon  10941  gruina  10942  axgroth2  10949  axgroth6  10952  grothac  10954  hashun2  14568  hashss  14594  hashsslei  14612  isercoll  15879  o1fsum  16024  incexc2  16051  znnen  16424  qnnen  16425  rpnnen  16439  ruc  16455  phicl2  16989  phibnd  16992  4sqlem11  17177  vdwlem11  17213  0ram  17242  mreexdomd  17873  pgpssslw  19879  fislw  19890  lindsdom  22211  cctop  23379  1stcfb  23818  2ndc1stc  23824  1stcrestlem  23825  2ndcctbss  23829  2ndcdisj2  23831  2ndcsep  23833  dis2ndc  23834  csdfil  24268  ufilen  24304  opnreen  25206  rectbntr0  25207  ovolctb2  25868  uniiccdif  25954  dyadmbl  25976  opnmblALT  25979  vitali  25989  mbfimaopnlem  26031  mbfsup  26040  fta1blem  26544  aannenlem3  26714  ppiwordi  27546  musum  27575  ppiub  27588  chpub  27604  dirith2  27912  upgrex  29727  rabfodom  33200  abrexdomjm  33202  mptctf  33405  locfinreflem  34583  esumcst  34806  omsmeas  35066  sibfof  35083  weexenwe  35889  j0ltalephlem  36048  subfaclefac  36149  erdszelem10  36173  snmlff  36302  finminlem  37321  iccioo01  38518  isinf2  38596  pibt2  38608  phpreu  38795  poimirlem26  38832  mblfinlem1  38843  abrexdom  38932  heiborlem3  39013  ctbnfien  44091  pellexlem4  44105  pellexlem5  44106  ttac  44309  idomodle  44454  idomsubgmo  44456  iscard5  44798  modelaxreplem1  46232  uzct  46354  rn1st  46558  smfaddlem2  48047  smfmullem4  48077  smfpimbor1lem1  48081  aacllem  51367