Theorem ssdomg 9032

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 5280	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 490	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6866	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6834	. . . . . . . . 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 6799	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6729	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 703	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6575	. . . . . . 7 ⊢ Fun I
12		cnvi 5863	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6563	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 234	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6620	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6546	. . . . 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 9001	. . 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 2144  Vcvv 3450   ⊆ wss 3896   class class class wbr 5102   I cid 5544  ^◡ccnv 5649   ↾ cres 5652  Fun wfun 6535  ⟶wf 6537  –1-1→wf1 6538  –onto→wfo 6539  –1-1-onto→wf1o 6540   ≼ cdom 8976

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7753

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-dom 8980

This theorem is used by:  cnvct  9067  xpdom3  9099  domunsncan  9101  domtriord  9147  sdomel  9148  sdomdif  9149  onsdominel  9150  pwdom  9153  2pwuninel  9156  mapdom1  9166  mapdom3  9173  limenpsi  9176  unbnn  9293  fidomdm  9328  hartogslem1  9541  hartogs  9543  card2on  9553  wdompwdom  9577  wdom2d  9579  wdomima2g  9585  unxpwdom2  9587  unxpwdom  9588  harwdom  9590  r1sdom  9786  tskwe  10036  carddomi2  10056  cardsdomelir  10059  cardsdomel  10060  harcard  10064  carduni  10067  cardmin2  10085  infxpenlem  10097  ssnum  10123  acnnum  10136  fodomfi2  10144  inffien  10147  alephordi  10158  dfac12lem2  10228  djudoml  10268  cdainflem  10271  djuinf  10272  unctb  10287  infunabs  10289  infdju  10290  infdif  10291  infdif2  10292  infmap2  10300  ackbij2  10325  fictb  10327  cfslb  10349  fincssdom  10406  fin67  10478  fin1a2lem12  10494  axcclem  10540  dmct  10607  dmctOLD  10608  brdom3  10612  brdom5  10613  brdom4  10614  imadomg  10618  imadomnum  10619  fnct  10625  fnctOLD  10626  mptct  10627  ondomon  10652  alephval2  10662  alephadd  10667  alephmul  10668  alephexp1  10669  alephsuc3  10670  alephexp2  10671  alephreg  10672  pwcfsdom  10673  cfpwsdom  10674  canthnum  10739  pwfseqlem5  10753  pwxpndom2  10755  pwdjundom  10757  gchaleph  10761  gchaleph2  10762  gchac  10771  winainflem  10783  gchina  10789  tsksdom  10846  tskinf  10859  inttsk  10864  inar1  10865  inatsk  10868  tskord  10870  tskcard  10871  grudomon  10907  gruina  10908  axgroth2  10915  axgroth6  10918  grothac  10920  hashun2  14532  hashss  14558  hashsslei  14576  isercoll  15842  o1fsum  15987  incexc2  16014  znnen  16387  qnnen  16388  rpnnen  16402  ruc  16418  phicl2  16952  phibnd  16955  4sqlem11  17140  vdwlem11  17176  0ram  17205  mreexdomd  17830  pgpssslw  19835  fislw  19846  lindsdom  22163  cctop  23331  1stcfb  23770  2ndc1stc  23776  1stcrestlem  23777  2ndcctbss  23781  2ndcdisj2  23783  2ndcsep  23785  dis2ndc  23786  csdfil  24220  ufilen  24256  opnreen  25158  rectbntr0  25159  ovolctb2  25820  uniiccdif  25906  dyadmbl  25928  opnmblALT  25931  vitali  25941  mbfimaopnlem  25983  mbfsup  25992  fta1blem  26496  aannenlem3  26664  ppiwordi  27496  musum  27525  ppiub  27538  chpub  27554  dirith2  27862  upgrex  29677  rabfodom  33150  abrexdomjm  33152  mptctf  33357  locfinreflem  34520  esumcst  34743  omsmeas  35003  sibfof  35020  weexenwe  35814  j0ltalephlem  35948  subfaclefac  36029  erdszelem10  36053  snmlff  36182  cardprcr  36552  finminlem  37200  iccioo01  38357  isinf2  38435  pibt2  38447  phpreu  38634  poimirlem26  38671  mblfinlem1  38682  abrexdom  38771  heiborlem3  38854  ctbnfien  43932  pellexlem4  43946  pellexlem5  43947  ttac  44150  idomodle  44300  idomsubgmo  44302  iscard5  44644  modelaxreplem1  46075  uzct  46187  rn1st  46392  smfaddlem2  47881  smfmullem4  47911  smfpimbor1lem1  47915  aacllem  51121