Theorem ssdomg 8547

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 5218	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 487	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6645	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6614	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 232	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 486	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6583	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6520	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 688	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6380	. . . . . . 7 ⊢ Fun I
12		cnvi 5993	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6369	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 233	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6424	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6353	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 592	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 483	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8519	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1366	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 416	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2108  Vcvv 3493   ⊆ wss 3934   class class class wbr 5057   I cid 5452  ^◡ccnv 5547   ↾ cres 5550  Fun wfun 6342  ⟶wf 6344  –1-1→wf1 6345  –onto→wfo 6346  –1-1-onto→wf1o 6347   ≼ cdom 8499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-dom 8503

This theorem is referenced by:  cnvct  8578  ssct  8590  undom  8597  xpdom3  8607  domunsncan  8609  0domg  8636  domtriord  8655  sdomel  8656  sdomdif  8657  onsdominel  8658  pwdom  8661  2pwuninel  8664  mapdom1  8674  mapdom3  8681  limenpsi  8684  php  8693  php2  8694  php3  8695  onomeneq  8700  nndomo  8704  sucdom2  8706  unbnn  8766  nnsdomg  8769  fodomfi  8789  fidomdm  8793  pwfilem  8810  hartogslem1  8998  hartogs  9000  card2on  9010  wdompwdom  9034  wdom2d  9036  wdomima2g  9042  unxpwdom2  9044  unxpwdom  9045  harwdom  9046  r1sdom  9195  tskwe  9371  carddomi2  9391  cardsdomelir  9394  cardsdomel  9395  harcard  9399  carduni  9402  cardmin2  9419  infxpenlem  9431  ssnum  9457  acnnum  9470  fodomfi2  9478  inffien  9481  alephordi  9492  dfac12lem2  9562  djudoml  9602  cdainflem  9605  djuinf  9606  unctb  9619  infunabs  9621  infdju  9622  infdif  9623  infdif2  9624  infmap2  9632  ackbij2  9657  fictb  9659  cfslb  9680  fincssdom  9737  fin67  9809  fin1a2lem12  9825  axcclem  9871  dmct  9938  brdom3  9942  brdom5  9943  brdom4  9944  imadomg  9948  fnct  9951  mptct  9952  ondomon  9977  alephval2  9986  alephadd  9991  alephmul  9992  alephexp1  9993  alephsuc3  9994  alephexp2  9995  alephreg  9996  pwcfsdom  9997  cfpwsdom  9998  canthnum  10063  pwfseqlem5  10077  pwxpndom2  10079  pwdjundom  10081  gchaleph  10085  gchaleph2  10086  gchac  10095  winainflem  10107  gchina  10113  tsksdom  10170  tskinf  10183  inttsk  10188  inar1  10189  inatsk  10192  tskord  10194  tskcard  10195  grudomon  10231  gruina  10232  axgroth2  10239  axgroth6  10242  grothac  10244  hashun2  13736  hashss  13762  hashsslei  13779  isercoll  15016  o1fsum  15160  incexc2  15185  znnen  15557  qnnen  15558  rpnnen  15572  ruc  15588  phicl2  16097  phibnd  16100  4sqlem11  16283  vdwlem11  16319  0ram  16348  mreexdomd  16912  pgpssslw  18731  fislw  18742  cctop  21606  1stcfb  22045  2ndc1stc  22051  1stcrestlem  22052  2ndcctbss  22055  2ndcdisj2  22057  2ndcsep  22059  dis2ndc  22060  csdfil  22494  ufilen  22530  opnreen  23431  rectbntr0  23432  ovolctb2  24085  uniiccdif  24171  dyadmbl  24193  opnmblALT  24196  vitali  24206  mbfimaopnlem  24248  mbfsup  24257  fta1blem  24754  aannenlem3  24911  ppiwordi  25731  musum  25760  ppiub  25772  chpub  25788  dirith2  26096  upgrex  26869  rabfodom  30258  abrexdomjm  30259  mptctf  30445  locfinreflem  31097  esumcst  31315  omsmeas  31574  sibfof  31591  subfaclefac  32416  erdszelem10  32440  snmlff  32569  finminlem  33659  isinf2  34678  pibt2  34690  phpreu  34868  lindsdom  34878  poimirlem26  34910  mblfinlem1  34921  abrexdom  34997  heiborlem3  35083  ctbnfien  39405  pellexlem4  39419  pellexlem5  39420  ttac  39623  idomodle  39786  idomsubgmo  39788  nndomog  39887  iscard5  39891  uzct  41315  smfaddlem2  43030  smfmullem4  43059  smfpimbor1lem1  43063  aacllem  44892