Theorem ssdomg 8974

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 5281	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6841	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6809	. . . . . . . . 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 6775	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6707	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 690	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6551	. . . . . . 7 ⊢ Fun I
12		cnvi 6117	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6540	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6596	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6519	. . . . 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 8944	. . 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 3450   ⊆ wss 3917   class class class wbr 5110   I cid 5535  ^◡ccnv 5640   ↾ cres 5643  Fun wfun 6508  ⟶wf 6510  –1-1→wf1 6511  –onto→wfo 6512  –1-1-onto→wf1o 6513   ≼ cdom 8919

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-dom 8923

This theorem is referenced by:  cnvct  9008  ssctOLD  9026  undomOLD  9034  xpdom3  9044  domunsncan  9046  sucdom2OLD  9056  domtriord  9093  sdomel  9094  sdomdif  9095  onsdominel  9096  pwdom  9099  2pwuninel  9102  mapdom1  9112  mapdom3  9119  limenpsi  9122  unbnn  9250  nnsdomgOLD  9254  fodomfiOLD  9288  fidomdm  9292  hartogslem1  9502  hartogs  9504  card2on  9514  wdompwdom  9538  wdom2d  9540  wdomima2g  9546  unxpwdom2  9548  unxpwdom  9549  harwdom  9551  r1sdom  9734  tskwe  9910  carddomi2  9930  cardsdomelir  9933  cardsdomel  9934  harcard  9938  carduni  9941  cardmin2  9959  infxpenlem  9973  ssnum  9999  acnnum  10012  fodomfi2  10020  inffien  10023  alephordi  10034  dfac12lem2  10105  djudoml  10145  cdainflem  10148  djuinf  10149  unctb  10164  infunabs  10166  infdju  10167  infdif  10168  infdif2  10169  infmap2  10177  ackbij2  10202  fictb  10204  cfslb  10226  fincssdom  10283  fin67  10355  fin1a2lem12  10371  axcclem  10417  dmct  10484  brdom3  10488  brdom5  10489  brdom4  10490  imadomg  10494  fnct  10497  mptct  10498  ondomon  10523  alephval2  10532  alephadd  10537  alephmul  10538  alephexp1  10539  alephsuc3  10540  alephexp2  10541  alephreg  10542  pwcfsdom  10543  cfpwsdom  10544  canthnum  10609  pwfseqlem5  10623  pwxpndom2  10625  pwdjundom  10627  gchaleph  10631  gchaleph2  10632  gchac  10641  winainflem  10653  gchina  10659  tsksdom  10716  tskinf  10729  inttsk  10734  inar1  10735  inatsk  10738  tskord  10740  tskcard  10741  grudomon  10777  gruina  10778  axgroth2  10785  axgroth6  10788  grothac  10790  hashun2  14355  hashss  14381  hashsslei  14398  isercoll  15641  o1fsum  15786  incexc2  15811  znnen  16187  qnnen  16188  rpnnen  16202  ruc  16218  phicl2  16745  phibnd  16748  4sqlem11  16933  vdwlem11  16969  0ram  16998  mreexdomd  17617  pgpssslw  19551  fislw  19562  cctop  22900  1stcfb  23339  2ndc1stc  23345  1stcrestlem  23346  2ndcctbss  23349  2ndcdisj2  23351  2ndcsep  23353  dis2ndc  23354  csdfil  23788  ufilen  23824  opnreen  24727  rectbntr0  24728  ovolctb2  25400  uniiccdif  25486  dyadmbl  25508  opnmblALT  25511  vitali  25521  mbfimaopnlem  25563  mbfsup  25572  fta1blem  26083  aannenlem3  26245  ppiwordi  27079  musum  27108  ppiub  27122  chpub  27138  dirith2  27446  upgrex  29026  rabfodom  32441  abrexdomjm  32443  mptctf  32648  locfinreflem  33837  esumcst  34060  omsmeas  34321  sibfof  34338  subfaclefac  35170  erdszelem10  35194  snmlff  35323  finminlem  36313  iccioo01  37322  isinf2  37400  pibt2  37412  phpreu  37605  lindsdom  37615  poimirlem26  37647  mblfinlem1  37658  abrexdom  37731  heiborlem3  37814  ctbnfien  42813  pellexlem4  42827  pellexlem5  42828  ttac  43032  idomodle  43187  idomsubgmo  43189  iscard5  43532  modelaxreplem1  44975  uzct  45064  rn1st  45274  smfaddlem2  46769  smfmullem4  46799  smfpimbor1lem1  46803  aacllem  49794