Theorem ssdomg 9006

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 5284	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 490	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6856	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6824	. . . . . . . . 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 6789	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6719	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 703	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6565	. . . . . . 7 ⊢ Fun I
12		cnvi 5865	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6554	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 234	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6610	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6538	. . . . 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 8975	. . 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 3450   ⊆ wss 3899   class class class wbr 5103   I cid 5549  ^◡ccnv 5654   ↾ cres 5657  Fun wfun 6527  ⟶wf 6529  –1-1→wf1 6530  –onto→wfo 6531  –1-1-onto→wf1o 6532   ≼ cdom 8950

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 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7736

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-dom 8954

This theorem is used by:  cnvct  9041  xpdom3  9073  domunsncan  9075  domtriord  9121  sdomel  9122  sdomdif  9123  onsdominel  9124  pwdom  9127  2pwuninel  9130  mapdom1  9140  mapdom3  9147  limenpsi  9150  unbnn  9266  fidomdm  9301  hartogslem1  9514  hartogs  9516  card2on  9526  wdompwdom  9550  wdom2d  9552  wdomima2g  9558  unxpwdom2  9560  unxpwdom  9561  harwdom  9563  r1sdom  9756  tskwe  9955  carddomi2  9975  cardsdomelir  9978  cardsdomel  9979  harcard  9983  carduni  9986  cardmin2  10004  infxpenlem  10016  ssnum  10042  acnnum  10055  fodomfi2  10063  inffien  10066  alephordi  10077  dfac12lem2  10147  djudoml  10187  cdainflem  10190  djuinf  10191  unctb  10206  infunabs  10208  infdju  10209  infdif  10210  infdif2  10211  infmap2  10219  ackbij2  10244  fictb  10246  cfslb  10268  fincssdom  10325  fin67  10397  fin1a2lem12  10413  axcclem  10459  dmct  10526  dmctOLD  10527  brdom3  10531  brdom5  10532  brdom4  10533  imadomg  10537  imadomnum  10538  fnct  10544  fnctOLD  10545  mptct  10546  ondomon  10571  alephval2  10581  alephadd  10586  alephmul  10587  alephexp1  10588  alephsuc3  10589  alephexp2  10590  alephreg  10591  pwcfsdom  10592  cfpwsdom  10593  canthnum  10658  pwfseqlem5  10672  pwxpndom2  10674  pwdjundom  10676  gchaleph  10680  gchaleph2  10681  gchac  10690  winainflem  10702  gchina  10708  tsksdom  10765  tskinf  10778  inttsk  10783  inar1  10784  inatsk  10787  tskord  10789  tskcard  10790  grudomon  10826  gruina  10827  axgroth2  10834  axgroth6  10837  grothac  10839  hashun2  14447  hashss  14473  hashsslei  14491  isercoll  15755  o1fsum  15900  incexc2  15927  znnen  16300  qnnen  16301  rpnnen  16315  ruc  16331  phicl2  16859  phibnd  16862  4sqlem11  17047  vdwlem11  17083  0ram  17112  mreexdomd  17737  pgpssslw  19741  fislw  19752  lindsdom  22063  cctop  23231  1stcfb  23670  2ndc1stc  23676  1stcrestlem  23677  2ndcctbss  23681  2ndcdisj2  23683  2ndcsep  23685  dis2ndc  23686  csdfil  24120  ufilen  24156  opnreen  25058  rectbntr0  25059  ovolctb2  25720  uniiccdif  25806  dyadmbl  25828  opnmblALT  25831  vitali  25841  mbfimaopnlem  25883  mbfsup  25892  fta1blem  26396  aannenlem3  26566  ppiwordi  27398  musum  27427  ppiub  27440  chpub  27456  dirith2  27764  upgrex  29549  rabfodom  32980  abrexdomjm  32982  mptctf  33187  locfinreflem  34350  esumcst  34573  omsmeas  34834  sibfof  34851  subfaclefac  35755  erdszelem10  35779  snmlff  35908  finminlem  36937  iccioo01  38081  isinf2  38159  pibt2  38171  phpreu  38358  poimirlem26  38395  mblfinlem1  38406  abrexdom  38480  heiborlem3  38563  ctbnfien  43659  pellexlem4  43673  pellexlem5  43674  ttac  43877  idomodle  44032  idomsubgmo  44034  iscard5  44376  modelaxreplem1  45801  uzct  45897  rn1st  46102  smfaddlem2  47592  smfmullem4  47622  smfpimbor1lem1  47626  aacllem  50772