Theorem ssdomg 8993

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 5290	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 489	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6859	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6827	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 233	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 488	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6792	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6722	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 702	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6568	. . . . . . 7 ⊢ Fun I
12		cnvi 5871	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6557	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 234	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6613	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6541	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 601	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 485	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8962	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1398	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 418	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3905   class class class wbr 5109   I cid 5555  ^◡ccnv 5660   ↾ cres 5663  Fun wfun 6530  ⟶wf 6532  –1-1→wf1 6533  –onto→wfo 6534  –1-1-onto→wf1o 6535   ≼ cdom 8937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-dom 8941

This theorem is referenced by:  cnvct  9027  xpdom3  9059  domunsncan  9061  domtriord  9107  sdomel  9108  sdomdif  9109  onsdominel  9110  pwdom  9113  2pwuninel  9116  mapdom1  9126  mapdom3  9133  limenpsi  9136  unbnn  9252  fidomdm  9287  hartogslem1  9500  hartogs  9502  card2on  9512  wdompwdom  9536  wdom2d  9538  wdomima2g  9544  unxpwdom2  9546  unxpwdom  9547  harwdom  9549  r1sdom  9742  tskwe  9932  carddomi2  9952  cardsdomelir  9955  cardsdomel  9956  harcard  9960  carduni  9963  cardmin2  9981  infxpenlem  9993  ssnum  10019  acnnum  10032  fodomfi2  10040  inffien  10043  alephordi  10054  dfac12lem2  10124  djudoml  10164  cdainflem  10167  djuinf  10168  unctb  10183  infunabs  10185  infdju  10186  infdif  10187  infdif2  10188  infmap2  10196  ackbij2  10221  fictb  10223  cfslb  10245  fincssdom  10302  fin67  10374  fin1a2lem12  10390  axcclem  10436  dmct  10503  brdom3  10507  brdom5  10508  brdom4  10509  imadomg  10513  fnct  10516  mptct  10517  ondomon  10542  alephval2  10552  alephadd  10557  alephmul  10558  alephexp1  10559  alephsuc3  10560  alephexp2  10561  alephreg  10562  pwcfsdom  10563  cfpwsdom  10564  canthnum  10629  pwfseqlem5  10643  pwxpndom2  10645  pwdjundom  10647  gchaleph  10651  gchaleph2  10652  gchac  10661  winainflem  10673  gchina  10679  tsksdom  10736  tskinf  10749  inttsk  10754  inar1  10755  inatsk  10758  tskord  10760  tskcard  10761  grudomon  10797  gruina  10798  axgroth2  10805  axgroth6  10808  grothac  10810  hashun2  14415  hashss  14441  hashsslei  14459  isercoll  15715  o1fsum  15861  incexc2  15888  znnen  16263  qnnen  16264  rpnnen  16278  ruc  16294  phicl2  16822  phibnd  16825  4sqlem11  17010  vdwlem11  17046  0ram  17075  mreexdomd  17700  pgpssslw  19679  fislw  19690  cctop  23163  1stcfb  23602  2ndc1stc  23608  1stcrestlem  23609  2ndcctbss  23612  2ndcdisj2  23614  2ndcsep  23616  dis2ndc  23617  csdfil  24051  ufilen  24087  opnreen  24989  rectbntr0  24990  ovolctb2  25651  uniiccdif  25737  dyadmbl  25759  opnmblALT  25762  vitali  25772  mbfimaopnlem  25814  mbfsup  25823  fta1blem  26328  aannenlem3  26493  ppiwordi  27326  musum  27355  ppiub  27368  chpub  27384  dirith2  27692  upgrex  29442  rabfodom  32851  abrexdomjm  32853  mptctf  33061  locfinreflem  34230  esumcst  34453  omsmeas  34713  sibfof  34730  subfaclefac  35668  erdszelem10  35692  snmlff  35821  finminlem  36829  iccioo01  37973  isinf2  38051  pibt2  38063  phpreu  38255  lindsdom  38265  poimirlem26  38297  mblfinlem1  38308  abrexdom  38381  heiborlem3  38464  ctbnfien  43545  pellexlem4  43559  pellexlem5  43560  ttac  43763  idomodle  43918  idomsubgmo  43920  iscard5  44262  modelaxreplem1  45687  uzct  45783  rn1st  45988  smfaddlem2  47478  smfmullem4  47508  smfpimbor1lem1  47512  aacllem  50621