Theorem ssdomg 8865

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 5271	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 486	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6809	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6777	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 229	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 485	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6743	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6672	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 688	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6520	. . . . . . 7 ⊢ Fun I
12		cnvi 6084	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6509	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 230	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6565	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6488	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 591	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 482	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8834	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1371	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 415	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2106  Vcvv 3442   ⊆ wss 3901   class class class wbr 5096   I cid 5521  ^◡ccnv 5623   ↾ cres 5626  Fun wfun 6477  ⟶wf 6479  –1-1→wf1 6480  –onto→wfo 6481  –1-1-onto→wf1o 6482   ≼ cdom 8806

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-opab 5159  df-id 5522  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-dom 8810

This theorem is referenced by:  cnvct  8903  ssctOLD  8921  undomOLD  8929  xpdom3  8939  domunsncan  8941  sucdom2OLD  8951  0domgOLD  8970  domtriord  8992  sdomel  8993  sdomdif  8994  onsdominel  8995  pwdom  8998  2pwuninel  9001  mapdom1  9011  mapdom3  9018  limenpsi  9021  phpOLD  9091  php2OLD  9092  php3OLD  9093  nndomogOLD  9095  onomeneqOLD  9098  unbnn  9168  nnsdomgOLD  9172  fodomfi  9194  fidomdm  9198  pwfilemOLD  9215  hartogslem1  9403  hartogs  9405  card2on  9415  wdompwdom  9439  wdom2d  9441  wdomima2g  9447  unxpwdom2  9449  unxpwdom  9450  harwdom  9452  r1sdom  9635  tskwe  9811  carddomi2  9831  cardsdomelir  9834  cardsdomel  9835  harcard  9839  carduni  9842  cardmin2  9860  infxpenlem  9874  ssnum  9900  acnnum  9913  fodomfi2  9921  inffien  9924  alephordi  9935  dfac12lem2  10005  djudoml  10045  cdainflem  10048  djuinf  10049  unctb  10066  infunabs  10068  infdju  10069  infdif  10070  infdif2  10071  infmap2  10079  ackbij2  10104  fictb  10106  cfslb  10127  fincssdom  10184  fin67  10256  fin1a2lem12  10272  axcclem  10318  dmct  10385  brdom3  10389  brdom5  10390  brdom4  10391  imadomg  10395  fnct  10398  mptct  10399  ondomon  10424  alephval2  10433  alephadd  10438  alephmul  10439  alephexp1  10440  alephsuc3  10441  alephexp2  10442  alephreg  10443  pwcfsdom  10444  cfpwsdom  10445  canthnum  10510  pwfseqlem5  10524  pwxpndom2  10526  pwdjundom  10528  gchaleph  10532  gchaleph2  10533  gchac  10542  winainflem  10554  gchina  10560  tsksdom  10617  tskinf  10630  inttsk  10635  inar1  10636  inatsk  10639  tskord  10641  tskcard  10642  grudomon  10678  gruina  10679  axgroth2  10686  axgroth6  10689  grothac  10691  hashun2  14202  hashss  14228  hashsslei  14245  isercoll  15478  o1fsum  15624  incexc2  15649  znnen  16020  qnnen  16021  rpnnen  16035  ruc  16051  phicl2  16566  phibnd  16569  4sqlem11  16753  vdwlem11  16789  0ram  16818  mreexdomd  17455  pgpssslw  19315  fislw  19326  cctop  22261  1stcfb  22701  2ndc1stc  22707  1stcrestlem  22708  2ndcctbss  22711  2ndcdisj2  22713  2ndcsep  22715  dis2ndc  22716  csdfil  23150  ufilen  23186  opnreen  24099  rectbntr0  24100  ovolctb2  24761  uniiccdif  24847  dyadmbl  24869  opnmblALT  24872  vitali  24882  mbfimaopnlem  24924  mbfsup  24933  fta1blem  25438  aannenlem3  25595  ppiwordi  26416  musum  26445  ppiub  26457  chpub  26473  dirith2  26781  upgrex  27750  rabfodom  31138  abrexdomjm  31139  mptctf  31337  locfinreflem  32086  esumcst  32327  omsmeas  32588  sibfof  32605  subfaclefac  33435  erdszelem10  33459  snmlff  33588  finminlem  34644  iccioo01  35652  isinf2  35730  pibt2  35742  phpreu  35917  lindsdom  35927  poimirlem26  35959  mblfinlem1  35970  abrexdom  36044  heiborlem3  36127  ctbnfien  40953  pellexlem4  40967  pellexlem5  40968  ttac  41172  idomodle  41335  idomsubgmo  41337  iscard5  41517  uzct  42983  smfaddlem2  44691  smfmullem4  44721  smfpimbor1lem1  44725  aacllem  46923