Theorem ssdomg 8948

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 5273	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6820	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6788	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 230	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 483	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6754	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6686	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 690	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6532	. . . . . . 7 ⊢ Fun I
12		cnvi 6102	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6521	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6577	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6504	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 590	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 480	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8918	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1373	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 413	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911   class class class wbr 5102   I cid 5525  ^◡ccnv 5630   ↾ cres 5633  Fun wfun 6493  ⟶wf 6495  –1-1→wf1 6496  –onto→wfo 6497  –1-1-onto→wf1o 6498   ≼ cdom 8893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-dom 8897

This theorem is referenced by:  cnvct  8982  xpdom3  9016  domunsncan  9018  domtriord  9064  sdomel  9065  sdomdif  9066  onsdominel  9067  pwdom  9070  2pwuninel  9073  mapdom1  9083  mapdom3  9090  limenpsi  9093  unbnn  9219  nnsdomgOLD  9223  fodomfiOLD  9257  fidomdm  9261  hartogslem1  9471  hartogs  9473  card2on  9483  wdompwdom  9507  wdom2d  9509  wdomima2g  9515  unxpwdom2  9517  unxpwdom  9518  harwdom  9520  r1sdom  9703  tskwe  9879  carddomi2  9899  cardsdomelir  9902  cardsdomel  9903  harcard  9907  carduni  9910  cardmin2  9928  infxpenlem  9942  ssnum  9968  acnnum  9981  fodomfi2  9989  inffien  9992  alephordi  10003  dfac12lem2  10074  djudoml  10114  cdainflem  10117  djuinf  10118  unctb  10133  infunabs  10135  infdju  10136  infdif  10137  infdif2  10138  infmap2  10146  ackbij2  10171  fictb  10173  cfslb  10195  fincssdom  10252  fin67  10324  fin1a2lem12  10340  axcclem  10386  dmct  10453  brdom3  10457  brdom5  10458  brdom4  10459  imadomg  10463  fnct  10466  mptct  10467  ondomon  10492  alephval2  10501  alephadd  10506  alephmul  10507  alephexp1  10508  alephsuc3  10509  alephexp2  10510  alephreg  10511  pwcfsdom  10512  cfpwsdom  10513  canthnum  10578  pwfseqlem5  10592  pwxpndom2  10594  pwdjundom  10596  gchaleph  10600  gchaleph2  10601  gchac  10610  winainflem  10622  gchina  10628  tsksdom  10685  tskinf  10698  inttsk  10703  inar1  10704  inatsk  10707  tskord  10709  tskcard  10710  grudomon  10746  gruina  10747  axgroth2  10754  axgroth6  10757  grothac  10759  hashun2  14324  hashss  14350  hashsslei  14367  isercoll  15610  o1fsum  15755  incexc2  15780  znnen  16156  qnnen  16157  rpnnen  16171  ruc  16187  phicl2  16714  phibnd  16717  4sqlem11  16902  vdwlem11  16938  0ram  16967  mreexdomd  17586  pgpssslw  19520  fislw  19531  cctop  22869  1stcfb  23308  2ndc1stc  23314  1stcrestlem  23315  2ndcctbss  23318  2ndcdisj2  23320  2ndcsep  23322  dis2ndc  23323  csdfil  23757  ufilen  23793  opnreen  24696  rectbntr0  24697  ovolctb2  25369  uniiccdif  25455  dyadmbl  25477  opnmblALT  25480  vitali  25490  mbfimaopnlem  25532  mbfsup  25541  fta1blem  26052  aannenlem3  26214  ppiwordi  27048  musum  27077  ppiub  27091  chpub  27107  dirith2  27415  upgrex  28995  rabfodom  32407  abrexdomjm  32409  mptctf  32614  locfinreflem  33803  esumcst  34026  omsmeas  34287  sibfof  34304  subfaclefac  35136  erdszelem10  35160  snmlff  35289  finminlem  36279  iccioo01  37288  isinf2  37366  pibt2  37378  phpreu  37571  lindsdom  37581  poimirlem26  37613  mblfinlem1  37624  abrexdom  37697  heiborlem3  37780  ctbnfien  42779  pellexlem4  42793  pellexlem5  42794  ttac  42998  idomodle  43153  idomsubgmo  43155  iscard5  43498  modelaxreplem1  44941  uzct  45030  rn1st  45240  smfaddlem2  46735  smfmullem4  46765  smfpimbor1lem1  46769  aacllem  49763