Theorem ssdomg 8999

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 5292	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 490	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6863	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6831	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 233	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 489	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6796	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6726	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 703	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6572	. . . . . . 7 ⊢ Fun I
12		cnvi 5873	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6561	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 234	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6617	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6545	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 602	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 486	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8968	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1398	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 419	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  Vcvv 3457   ⊆ wss 3906   class class class wbr 5111   I cid 5557  ^◡ccnv 5662   ↾ cres 5665  Fun wfun 6534  ⟶wf 6536  –1-1→wf1 6537  –onto→wfo 6538  –1-1-onto→wf1o 6539   ≼ cdom 8943

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pow 5338  ax-pr 5406  ax-un 7738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-dom 8947

This theorem is used by:  cnvct  9034  xpdom3  9066  domunsncan  9068  domtriord  9114  sdomel  9115  sdomdif  9116  onsdominel  9117  pwdom  9120  2pwuninel  9123  mapdom1  9133  mapdom3  9140  limenpsi  9143  unbnn  9259  fidomdm  9294  hartogslem1  9507  hartogs  9509  card2on  9519  wdompwdom  9543  wdom2d  9545  wdomima2g  9551  unxpwdom2  9553  unxpwdom  9554  harwdom  9556  r1sdom  9749  tskwe  9948  carddomi2  9968  cardsdomelir  9971  cardsdomel  9972  harcard  9976  carduni  9979  cardmin2  9997  infxpenlem  10009  ssnum  10035  acnnum  10048  fodomfi2  10056  inffien  10059  alephordi  10070  dfac12lem2  10140  djudoml  10180  cdainflem  10183  djuinf  10184  unctb  10199  infunabs  10201  infdju  10202  infdif  10203  infdif2  10204  infmap2  10212  ackbij2  10237  fictb  10239  cfslb  10261  fincssdom  10318  fin67  10390  fin1a2lem12  10406  axcclem  10452  dmct  10519  brdom3  10523  brdom5  10524  brdom4  10525  imadomg  10529  fnct  10532  mptct  10533  ondomon  10558  alephval2  10568  alephadd  10573  alephmul  10574  alephexp1  10575  alephsuc3  10576  alephexp2  10577  alephreg  10578  pwcfsdom  10579  cfpwsdom  10580  canthnum  10645  pwfseqlem5  10659  pwxpndom2  10661  pwdjundom  10663  gchaleph  10667  gchaleph2  10668  gchac  10677  winainflem  10689  gchina  10695  tsksdom  10752  tskinf  10765  inttsk  10770  inar1  10771  inatsk  10774  tskord  10776  tskcard  10777  grudomon  10813  gruina  10814  axgroth2  10821  axgroth6  10824  grothac  10826  hashun2  14433  hashss  14459  hashsslei  14477  isercoll  15739  o1fsum  15884  incexc2  15911  znnen  16286  qnnen  16287  rpnnen  16301  ruc  16317  phicl2  16845  phibnd  16848  4sqlem11  17033  vdwlem11  17069  0ram  17098  mreexdomd  17723  pgpssslw  19708  fislw  19719  cctop  23193  1stcfb  23632  2ndc1stc  23638  1stcrestlem  23639  2ndcctbss  23643  2ndcdisj2  23645  2ndcsep  23647  dis2ndc  23648  csdfil  24082  ufilen  24118  opnreen  25020  rectbntr0  25021  ovolctb2  25682  uniiccdif  25768  dyadmbl  25790  opnmblALT  25793  vitali  25803  mbfimaopnlem  25845  mbfsup  25854  fta1blem  26359  aannenlem3  26524  ppiwordi  27357  musum  27386  ppiub  27399  chpub  27415  dirith2  27723  upgrex  29473  rabfodom  32898  abrexdomjm  32900  mptctf  33107  locfinreflem  34270  esumcst  34493  omsmeas  34754  sibfof  34771  subfaclefac  35681  erdszelem10  35705  snmlff  35834  finminlem  36862  iccioo01  38006  isinf2  38084  pibt2  38096  phpreu  38288  lindsdom  38298  poimirlem26  38330  mblfinlem1  38341  abrexdom  38414  heiborlem3  38497  ctbnfien  43578  pellexlem4  43592  pellexlem5  43593  ttac  43796  idomodle  43951  idomsubgmo  43953  iscard5  44295  modelaxreplem1  45720  uzct  45816  rn1st  46021  smfaddlem2  47511  smfmullem4  47541  smfpimbor1lem1  47545  aacllem  50654