Theorem ssdomg 8975

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 5276	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 488	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6840	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6808	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 232	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 487	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6773	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6703	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 700	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6548	. . . . . . 7 ⊢ Fun I
12		cnvi 5853	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6537	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 233	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6593	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6521	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 599	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8944	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1389	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 417	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3902   class class class wbr 5097   I cid 5537  ^◡ccnv 5642   ↾ cres 5645  Fun wfun 6510  ⟶wf 6512  –1-1→wf1 6513  –onto→wfo 6514  –1-1-onto→wf1o 6515   ≼ cdom 8919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pow 5319  ax-pr 5387  ax-un 7713

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-dom 8923

This theorem is referenced by:  cnvct  9009  xpdom3  9041  domunsncan  9043  domtriord  9089  sdomel  9090  sdomdif  9091  onsdominel  9092  pwdom  9095  2pwuninel  9098  mapdom1  9108  mapdom3  9115  limenpsi  9118  unbnn  9234  fidomdm  9271  hartogslem1  9484  hartogs  9486  card2on  9496  wdompwdom  9520  wdom2d  9522  wdomima2g  9528  unxpwdom2  9530  unxpwdom  9531  harwdom  9533  r1sdom  9726  tskwe  9902  carddomi2  9922  cardsdomelir  9925  cardsdomel  9926  harcard  9930  carduni  9933  cardmin2  9951  infxpenlem  9963  ssnum  9989  acnnum  10002  fodomfi2  10010  inffien  10013  alephordi  10024  dfac12lem2  10095  djudoml  10135  cdainflem  10138  djuinf  10139  unctb  10154  infunabs  10156  infdju  10157  infdif  10158  infdif2  10159  infmap2  10167  ackbij2  10192  fictb  10194  cfslb  10217  fincssdom  10274  fin67  10346  fin1a2lem12  10362  axcclem  10408  dmct  10475  brdom3  10479  brdom5  10480  brdom4  10481  imadomg  10485  fnct  10488  mptct  10489  ondomon  10514  alephval2  10524  alephadd  10529  alephmul  10530  alephexp1  10531  alephsuc3  10532  alephexp2  10533  alephreg  10534  pwcfsdom  10535  cfpwsdom  10536  canthnum  10601  pwfseqlem5  10615  pwxpndom2  10617  pwdjundom  10619  gchaleph  10623  gchaleph2  10624  gchac  10633  winainflem  10645  gchina  10651  tsksdom  10708  tskinf  10721  inttsk  10726  inar1  10727  inatsk  10730  tskord  10732  tskcard  10733  grudomon  10769  gruina  10770  axgroth2  10777  axgroth6  10780  grothac  10782  hashun2  14390  hashss  14416  hashsslei  14433  isercoll  15686  o1fsum  15832  incexc2  15859  znnen  16235  qnnen  16236  rpnnen  16250  ruc  16266  phicl2  16794  phibnd  16797  4sqlem11  16982  vdwlem11  17018  0ram  17047  mreexdomd  17672  pgpssslw  19645  fislw  19656  cctop  23054  1stcfb  23493  2ndc1stc  23499  1stcrestlem  23500  2ndcctbss  23503  2ndcdisj2  23505  2ndcsep  23507  dis2ndc  23508  csdfil  23942  ufilen  23978  opnreen  24880  rectbntr0  24881  ovolctb2  25542  uniiccdif  25628  dyadmbl  25650  opnmblALT  25653  vitali  25663  mbfimaopnlem  25705  mbfsup  25714  fta1blem  26219  aannenlem3  26382  ppiwordi  27214  musum  27243  ppiub  27256  chpub  27272  dirith2  27580  upgrex  29250  rabfodom  32664  abrexdomjm  32666  mptctf  32879  locfinreflem  34098  esumcst  34321  omsmeas  34581  sibfof  34598  subfaclefac  35487  erdszelem10  35511  snmlff  35640  finminlem  36639  iccioo01  37782  isinf2  37860  pibt2  37872  phpreu  38064  lindsdom  38074  poimirlem26  38106  mblfinlem1  38117  abrexdom  38190  heiborlem3  38273  ctbnfien  43356  pellexlem4  43370  pellexlem5  43371  ttac  43574  idomodle  43729  idomsubgmo  43731  iscard5  44073  modelaxreplem1  45515  uzct  45604  rn1st  45809  smfaddlem2  47299  smfmullem4  47329  smfpimbor1lem1  47333  aacllem  50383