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 5291	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 489	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6857	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6825	. . . . . . . . 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 6790	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6720	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 702	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6566	. . . . . . 7 ⊢ Fun I
12		cnvi 5869	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6555	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 234	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6611	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6539	. . . . 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 1396	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 418	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  Vcvv 3463   ⊆ wss 3913   class class class wbr 5110   I cid 5553  ^◡ccnv 5658   ↾ cres 5661  Fun wfun 6528  ⟶wf 6530  –1-1→wf1 6531  –onto→wfo 6532  –1-1-onto→wf1o 6533   ≼ cdom 8937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pow 5334  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-dom 8941

This theorem is referenced 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  9932  carddomi2  9952  cardsdomelir  9955  cardsdomel  9956  harcard  9960  carduni  9963  cardmin2  9981  infxpenlem  9993  ssnum  10019  acnnum  10032  fodomfi2  10040  inffien  10043  alephordi  10054  dfac12lem2  10124  djudoml  10164  cdainflem  10167  djuinf  10168  unctb  10183  infunabs  10185  infdju  10186  infdif  10187  infdif2  10188  infmap2  10196  ackbij2  10221  fictb  10223  cfslb  10246  fincssdom  10303  fin67  10375  fin1a2lem12  10391  axcclem  10437  dmct  10504  brdom3  10508  brdom5  10509  brdom4  10510  imadomg  10514  fnct  10517  mptct  10518  ondomon  10543  alephval2  10553  alephadd  10558  alephmul  10559  alephexp1  10560  alephsuc3  10561  alephexp2  10562  alephreg  10563  pwcfsdom  10564  cfpwsdom  10565  canthnum  10630  pwfseqlem5  10644  pwxpndom2  10646  pwdjundom  10648  gchaleph  10652  gchaleph2  10653  gchac  10662  winainflem  10674  gchina  10680  tsksdom  10737  tskinf  10750  inttsk  10755  inar1  10756  inatsk  10759  tskord  10761  tskcard  10762  grudomon  10798  gruina  10799  axgroth2  10806  axgroth6  10809  grothac  10811  hashun2  14415  hashss  14441  hashsslei  14459  isercoll  15715  o1fsum  15861  incexc2  15888  znnen  16264  qnnen  16265  rpnnen  16279  ruc  16295  phicl2  16823  phibnd  16826  4sqlem11  17011  vdwlem11  17047  0ram  17076  mreexdomd  17701  pgpssslw  19680  fislw  19691  cctop  23128  1stcfb  23567  2ndc1stc  23573  1stcrestlem  23574  2ndcctbss  23577  2ndcdisj2  23579  2ndcsep  23581  dis2ndc  23582  csdfil  24016  ufilen  24052  opnreen  24954  rectbntr0  24955  ovolctb2  25616  uniiccdif  25702  dyadmbl  25724  opnmblALT  25727  vitali  25737  mbfimaopnlem  25779  mbfsup  25788  fta1blem  26293  aannenlem3  26456  ppiwordi  27288  musum  27317  ppiub  27330  chpub  27346  dirith2  27654  upgrex  29379  rabfodom  32788  abrexdomjm  32790  mptctf  32998  locfinreflem  34171  esumcst  34394  omsmeas  34654  sibfof  34671  subfaclefac  35563  erdszelem10  35587  snmlff  35716  finminlem  36714  iccioo01  37856  isinf2  37934  pibt2  37946  phpreu  38138  lindsdom  38148  poimirlem26  38180  mblfinlem1  38191  abrexdom  38264  heiborlem3  38347  ctbnfien  43432  pellexlem4  43446  pellexlem5  43447  ttac  43650  idomodle  43805  idomsubgmo  43807  iscard5  44149  modelaxreplem1  45574  uzct  45670  rn1st  45875  smfaddlem2  47365  smfmullem4  47395  smfpimbor1lem1  47399  aacllem  50470