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 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

This proof depends on syntax axioms:   → 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 proof depends on 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 proof 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 used 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  9941  carddomi2  9961  cardsdomelir  9964  cardsdomel  9965  harcard  9969  carduni  9972  cardmin2  9990  infxpenlem  10002  ssnum  10028  acnnum  10041  fodomfi2  10049  inffien  10052  alephordi  10063  dfac12lem2  10133  djudoml  10173  cdainflem  10176  djuinf  10177  unctb  10192  infunabs  10194  infdju  10195  infdif  10196  infdif2  10197  infmap2  10205  ackbij2  10230  fictb  10232  cfslb  10254  fincssdom  10311  fin67  10383  fin1a2lem12  10399  axcclem  10445  dmct  10512  brdom3  10516  brdom5  10517  brdom4  10518  imadomg  10522  fnct  10525  mptct  10526  ondomon  10551  alephval2  10561  alephadd  10566  alephmul  10567  alephexp1  10568  alephsuc3  10569  alephexp2  10570  alephreg  10571  pwcfsdom  10572  cfpwsdom  10573  canthnum  10638  pwfseqlem5  10652  pwxpndom2  10654  pwdjundom  10656  gchaleph  10660  gchaleph2  10661  gchac  10670  winainflem  10682  gchina  10688  tsksdom  10745  tskinf  10758  inttsk  10763  inar1  10764  inatsk  10767  tskord  10769  tskcard  10770  grudomon  10806  gruina  10807  axgroth2  10814  axgroth6  10817  grothac  10819  hashun2  14424  hashss  14450  hashsslei  14468  isercoll  15724  o1fsum  15870  incexc2  15897  znnen  16272  qnnen  16273  rpnnen  16287  ruc  16303  phicl2  16831  phibnd  16834  4sqlem11  17019  vdwlem11  17055  0ram  17084  mreexdomd  17709  pgpssslw  19688  fislw  19699  cctop  23172  1stcfb  23611  2ndc1stc  23617  1stcrestlem  23618  2ndcctbss  23621  2ndcdisj2  23623  2ndcsep  23625  dis2ndc  23626  csdfil  24060  ufilen  24096  opnreen  24998  rectbntr0  24999  ovolctb2  25660  uniiccdif  25746  dyadmbl  25768  opnmblALT  25771  vitali  25781  mbfimaopnlem  25823  mbfsup  25832  fta1blem  26337  aannenlem3  26502  ppiwordi  27335  musum  27364  ppiub  27377  chpub  27393  dirith2  27701  upgrex  29451  rabfodom  32860  abrexdomjm  32862  mptctf  33070  locfinreflem  34239  esumcst  34462  omsmeas  34722  sibfof  34739  subfaclefac  35676  erdszelem10  35700  snmlff  35829  finminlem  36857  iccioo01  38001  isinf2  38079  pibt2  38091  phpreu  38283  lindsdom  38293  poimirlem26  38325  mblfinlem1  38336  abrexdom  38409  heiborlem3  38492  ctbnfien  43573  pellexlem4  43587  pellexlem5  43588  ttac  43791  idomodle  43946  idomsubgmo  43948  iscard5  44290  modelaxreplem1  45715  uzct  45811  rn1st  46016  smfaddlem2  47506  smfmullem4  47536  smfpimbor1lem1  47540  aacllem  50649