Theorem ssdomg 8925

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 5262	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6802	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6770	. . . . . . . . 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 6736	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6668	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 690	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6514	. . . . . . 7 ⊢ Fun I
12		cnvi 6090	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6503	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6559	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6487	. . . . 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 8895	. . 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 3436   ⊆ wss 3903   class class class wbr 5092   I cid 5513  ^◡ccnv 5618   ↾ cres 5621  Fun wfun 6476  ⟶wf 6478  –1-1→wf1 6479  –onto→wfo 6480  –1-1-onto→wf1o 6481   ≼ cdom 8870

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-dom 8874

This theorem is referenced by:  cnvct  8959  xpdom3  8992  domunsncan  8994  domtriord  9040  sdomel  9041  sdomdif  9042  onsdominel  9043  pwdom  9046  2pwuninel  9049  mapdom1  9059  mapdom3  9066  limenpsi  9069  unbnn  9185  fodomfiOLD  9220  fidomdm  9224  hartogslem1  9434  hartogs  9436  card2on  9446  wdompwdom  9470  wdom2d  9472  wdomima2g  9478  unxpwdom2  9480  unxpwdom  9481  harwdom  9483  r1sdom  9670  tskwe  9846  carddomi2  9866  cardsdomelir  9869  cardsdomel  9870  harcard  9874  carduni  9877  cardmin2  9895  infxpenlem  9907  ssnum  9933  acnnum  9946  fodomfi2  9954  inffien  9957  alephordi  9968  dfac12lem2  10039  djudoml  10079  cdainflem  10082  djuinf  10083  unctb  10098  infunabs  10100  infdju  10101  infdif  10102  infdif2  10103  infmap2  10111  ackbij2  10136  fictb  10138  cfslb  10160  fincssdom  10217  fin67  10289  fin1a2lem12  10305  axcclem  10351  dmct  10418  brdom3  10422  brdom5  10423  brdom4  10424  imadomg  10428  fnct  10431  mptct  10432  ondomon  10457  alephval2  10466  alephadd  10471  alephmul  10472  alephexp1  10473  alephsuc3  10474  alephexp2  10475  alephreg  10476  pwcfsdom  10477  cfpwsdom  10478  canthnum  10543  pwfseqlem5  10557  pwxpndom2  10559  pwdjundom  10561  gchaleph  10565  gchaleph2  10566  gchac  10575  winainflem  10587  gchina  10593  tsksdom  10650  tskinf  10663  inttsk  10668  inar1  10669  inatsk  10672  tskord  10674  tskcard  10675  grudomon  10711  gruina  10712  axgroth2  10719  axgroth6  10722  grothac  10724  hashun2  14290  hashss  14316  hashsslei  14333  isercoll  15575  o1fsum  15720  incexc2  15745  znnen  16121  qnnen  16122  rpnnen  16136  ruc  16152  phicl2  16679  phibnd  16682  4sqlem11  16867  vdwlem11  16903  0ram  16932  mreexdomd  17555  pgpssslw  19493  fislw  19504  cctop  22891  1stcfb  23330  2ndc1stc  23336  1stcrestlem  23337  2ndcctbss  23340  2ndcdisj2  23342  2ndcsep  23344  dis2ndc  23345  csdfil  23779  ufilen  23815  opnreen  24718  rectbntr0  24719  ovolctb2  25391  uniiccdif  25477  dyadmbl  25499  opnmblALT  25502  vitali  25512  mbfimaopnlem  25554  mbfsup  25563  fta1blem  26074  aannenlem3  26236  ppiwordi  27070  musum  27099  ppiub  27113  chpub  27129  dirith2  27437  upgrex  29037  rabfodom  32449  abrexdomjm  32451  mptctf  32660  locfinreflem  33807  esumcst  34030  omsmeas  34291  sibfof  34308  subfaclefac  35153  erdszelem10  35177  snmlff  35306  finminlem  36296  iccioo01  37305  isinf2  37383  pibt2  37395  phpreu  37588  lindsdom  37598  poimirlem26  37630  mblfinlem1  37641  abrexdom  37714  heiborlem3  37797  ctbnfien  42795  pellexlem4  42809  pellexlem5  42810  ttac  43013  idomodle  43168  idomsubgmo  43170  iscard5  43513  modelaxreplem1  44956  uzct  45045  rn1st  45255  smfaddlem2  46749  smfmullem4  46779  smfpimbor1lem1  46783  aacllem  49790