Theorem ssdomg 8947

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 5264	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6818	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6786	. . . . . . . . 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 6752	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6684	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 691	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6530	. . . . . . 7 ⊢ Fun I
12		cnvi 6105	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6519	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6575	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6503	. . . . 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 8916	. . 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 3429   ⊆ wss 3889   class class class wbr 5085   I cid 5525  ^◡ccnv 5630   ↾ cres 5633  Fun wfun 6492  ⟶wf 6494  –1-1→wf1 6495  –onto→wfo 6496  –1-1-onto→wf1o 6497   ≼ cdom 8891

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 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-dom 8895

This theorem is referenced by:  cnvct  8981  xpdom3  9013  domunsncan  9015  domtriord  9061  sdomel  9062  sdomdif  9063  onsdominel  9064  pwdom  9067  2pwuninel  9070  mapdom1  9080  mapdom3  9087  limenpsi  9090  unbnn  9206  fodomfiOLD  9240  fidomdm  9244  hartogslem1  9457  hartogs  9459  card2on  9469  wdompwdom  9493  wdom2d  9495  wdomima2g  9501  unxpwdom2  9503  unxpwdom  9504  harwdom  9506  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  14345  hashss  14371  hashsslei  14388  isercoll  15630  o1fsum  15776  incexc2  15803  znnen  16179  qnnen  16180  rpnnen  16194  ruc  16210  phicl2  16738  phibnd  16741  4sqlem11  16926  vdwlem11  16962  0ram  16991  mreexdomd  17615  pgpssslw  19589  fislw  19600  cctop  22971  1stcfb  23410  2ndc1stc  23416  1stcrestlem  23417  2ndcctbss  23420  2ndcdisj2  23422  2ndcsep  23424  dis2ndc  23425  csdfil  23859  ufilen  23895  opnreen  24797  rectbntr0  24798  ovolctb2  25459  uniiccdif  25545  dyadmbl  25567  opnmblALT  25570  vitali  25580  mbfimaopnlem  25622  mbfsup  25631  fta1blem  26136  aannenlem3  26296  ppiwordi  27125  musum  27154  ppiub  27167  chpub  27183  dirith2  27491  upgrex  29161  rabfodom  32575  abrexdomjm  32577  mptctf  32789  locfinreflem  33984  esumcst  34207  omsmeas  34467  sibfof  34484  subfaclefac  35358  erdszelem10  35382  snmlff  35511  finminlem  36500  iccioo01  37643  isinf2  37721  pibt2  37733  phpreu  37925  lindsdom  37935  poimirlem26  37967  mblfinlem1  37978  abrexdom  38051  heiborlem3  38134  ctbnfien  43246  pellexlem4  43260  pellexlem5  43261  ttac  43464  idomodle  43619  idomsubgmo  43621  iscard5  43963  modelaxreplem1  45405  uzct  45494  rn1st  45702  smfaddlem2  47192  smfmullem4  47222  smfpimbor1lem1  47226  aacllem  50276