Theorem ssdomg 9020

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 5281	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 490	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6861	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6829	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 233	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 489	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6794	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6724	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 703	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6570	. . . . . . 7 ⊢ Fun I
12		cnvi 5863	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6558	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 234	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6615	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6542	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 602	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 486	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8989	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1398	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 419	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Vcvv 3451   ⊆ wss 3899   class class class wbr 5103   I cid 5545  ^◡ccnv 5650   ↾ cres 5653  Fun wfun 6531  ⟶wf 6533  –1-1→wf1 6534  –onto→wfo 6535  –1-1-onto→wf1o 6536   ≼ cdom 8964

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-dom 8968

This theorem is used by:  cnvct  9055  xpdom3  9087  domunsncan  9089  domtriord  9135  sdomel  9136  sdomdif  9137  onsdominel  9138  pwdom  9141  2pwuninel  9144  mapdom1  9154  mapdom3  9161  limenpsi  9164  unbnn  9281  fidomdm  9316  hartogslem1  9529  hartogs  9531  card2on  9541  wdompwdom  9565  wdom2d  9567  wdomima2g  9573  unxpwdom2  9575  unxpwdom  9576  harwdom  9578  r1sdom  9774  tskwe  10024  carddomi2  10044  cardsdomelir  10047  cardsdomel  10048  harcard  10052  carduni  10055  cardmin2  10073  infxpenlem  10085  ssnum  10111  acnnum  10124  fodomfi2  10132  inffien  10135  alephordi  10146  dfac12lem2  10216  djudoml  10256  cdainflem  10259  djuinf  10260  unctb  10275  infunabs  10277  infdju  10278  infdif  10279  infdif2  10280  infmap2  10288  ackbij2  10313  fictb  10315  cfslb  10337  fincssdom  10394  fin67  10466  fin1a2lem12  10482  axcclem  10528  dmct  10595  dmctOLD  10596  brdom3  10600  brdom5  10601  brdom4  10602  imadomg  10606  imadomnum  10607  fnct  10613  fnctOLD  10614  mptct  10615  ondomon  10640  alephval2  10650  alephadd  10655  alephmul  10656  alephexp1  10657  alephsuc3  10658  alephexp2  10659  alephreg  10660  pwcfsdom  10661  cfpwsdom  10662  canthnum  10727  pwfseqlem5  10741  pwxpndom2  10743  pwdjundom  10745  gchaleph  10749  gchaleph2  10750  gchac  10759  winainflem  10771  gchina  10777  tsksdom  10834  tskinf  10847  inttsk  10852  inar1  10853  inatsk  10856  tskord  10858  tskcard  10859  grudomon  10895  gruina  10896  axgroth2  10903  axgroth6  10906  grothac  10908  hashun2  14520  hashss  14546  hashsslei  14564  isercoll  15828  o1fsum  15973  incexc2  16000  znnen  16373  qnnen  16374  rpnnen  16388  ruc  16404  phicl2  16938  phibnd  16941  4sqlem11  17126  vdwlem11  17162  0ram  17191  mreexdomd  17816  pgpssslw  19821  fislw  19832  lindsdom  22149  cctop  23317  1stcfb  23756  2ndc1stc  23762  1stcrestlem  23763  2ndcctbss  23767  2ndcdisj2  23769  2ndcsep  23771  dis2ndc  23772  csdfil  24206  ufilen  24242  opnreen  25144  rectbntr0  25145  ovolctb2  25806  uniiccdif  25892  dyadmbl  25914  opnmblALT  25917  vitali  25927  mbfimaopnlem  25969  mbfsup  25978  fta1blem  26482  aannenlem3  26650  ppiwordi  27482  musum  27511  ppiub  27524  chpub  27540  dirith2  27848  upgrex  29663  rabfodom  33094  abrexdomjm  33096  mptctf  33301  locfinreflem  34465  esumcst  34688  omsmeas  34948  sibfof  34965  subfaclefac  35920  erdszelem10  35944  snmlff  36073  finminlem  37086  iccioo01  38230  isinf2  38308  pibt2  38320  phpreu  38507  poimirlem26  38544  mblfinlem1  38555  abrexdom  38644  heiborlem3  38727  ctbnfien  43804  pellexlem4  43818  pellexlem5  43819  ttac  44022  idomodle  44177  idomsubgmo  44179  iscard5  44521  modelaxreplem1  45946  uzct  46049  rn1st  46254  smfaddlem2  47743  smfmullem4  47773  smfpimbor1lem1  47777  aacllem  50908