Theorem ssdomg 8949

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 5270	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6820	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6788	. . . . . . . . 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 6754	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6686	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 691	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6532	. . . . . . 7 ⊢ Fun I
12		cnvi 6107	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6521	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6577	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6505	. . . . 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 8918	. . 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 3442   ⊆ wss 3903   class class class wbr 5100   I cid 5526  ^◡ccnv 5631   ↾ cres 5634  Fun wfun 6494  ⟶wf 6496  –1-1→wf1 6497  –onto→wfo 6498  –1-1-onto→wf1o 6499   ≼ cdom 8893

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 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-dom 8897

This theorem is referenced by:  cnvct  8983  xpdom3  9015  domunsncan  9017  domtriord  9063  sdomel  9064  sdomdif  9065  onsdominel  9066  pwdom  9069  2pwuninel  9072  mapdom1  9082  mapdom3  9089  limenpsi  9092  unbnn  9208  fodomfiOLD  9242  fidomdm  9246  hartogslem1  9459  hartogs  9461  card2on  9471  wdompwdom  9495  wdom2d  9497  wdomima2g  9503  unxpwdom2  9505  unxpwdom  9506  harwdom  9508  r1sdom  9698  tskwe  9874  carddomi2  9894  cardsdomelir  9897  cardsdomel  9898  harcard  9902  carduni  9905  cardmin2  9923  infxpenlem  9935  ssnum  9961  acnnum  9974  fodomfi2  9982  inffien  9985  alephordi  9996  dfac12lem2  10067  djudoml  10107  cdainflem  10110  djuinf  10111  unctb  10126  infunabs  10128  infdju  10129  infdif  10130  infdif2  10131  infmap2  10139  ackbij2  10164  fictb  10166  cfslb  10188  fincssdom  10245  fin67  10317  fin1a2lem12  10333  axcclem  10379  dmct  10446  brdom3  10450  brdom5  10451  brdom4  10452  imadomg  10456  fnct  10459  mptct  10460  ondomon  10485  alephval2  10495  alephadd  10500  alephmul  10501  alephexp1  10502  alephsuc3  10503  alephexp2  10504  alephreg  10505  pwcfsdom  10506  cfpwsdom  10507  canthnum  10572  pwfseqlem5  10586  pwxpndom2  10588  pwdjundom  10590  gchaleph  10594  gchaleph2  10595  gchac  10604  winainflem  10616  gchina  10622  tsksdom  10679  tskinf  10692  inttsk  10697  inar1  10698  inatsk  10701  tskord  10703  tskcard  10704  grudomon  10740  gruina  10741  axgroth2  10748  axgroth6  10751  grothac  10753  hashun2  14318  hashss  14344  hashsslei  14361  isercoll  15603  o1fsum  15748  incexc2  15773  znnen  16149  qnnen  16150  rpnnen  16164  ruc  16180  phicl2  16707  phibnd  16710  4sqlem11  16895  vdwlem11  16931  0ram  16960  mreexdomd  17584  pgpssslw  19555  fislw  19566  cctop  22962  1stcfb  23401  2ndc1stc  23407  1stcrestlem  23408  2ndcctbss  23411  2ndcdisj2  23413  2ndcsep  23415  dis2ndc  23416  csdfil  23850  ufilen  23886  opnreen  24788  rectbntr0  24789  ovolctb2  25461  uniiccdif  25547  dyadmbl  25569  opnmblALT  25572  vitali  25582  mbfimaopnlem  25624  mbfsup  25633  fta1blem  26144  aannenlem3  26306  ppiwordi  27140  musum  27169  ppiub  27183  chpub  27199  dirith2  27507  upgrex  29177  rabfodom  32592  abrexdomjm  32594  mptctf  32806  locfinreflem  34018  esumcst  34241  omsmeas  34501  sibfof  34518  subfaclefac  35392  erdszelem10  35416  snmlff  35545  finminlem  36534  iccioo01  37582  isinf2  37660  pibt2  37672  phpreu  37855  lindsdom  37865  poimirlem26  37897  mblfinlem1  37908  abrexdom  37981  heiborlem3  38064  ctbnfien  43175  pellexlem4  43189  pellexlem5  43190  ttac  43393  idomodle  43548  idomsubgmo  43550  iscard5  43892  modelaxreplem1  45334  uzct  45423  rn1st  45631  smfaddlem2  47122  smfmullem4  47152  smfpimbor1lem1  47156  aacllem  50160