Theorem ssdomg 8937

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 5268	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6812	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6780	. . . . . . . . 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 6746	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6678	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 690	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6524	. . . . . . 7 ⊢ Fun I
12		cnvi 6099	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6513	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6569	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6497	. . . . 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 8906	. . 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 2113  Vcvv 3440   ⊆ wss 3901   class class class wbr 5098   I cid 5518  ^◡ccnv 5623   ↾ cres 5626  Fun wfun 6486  ⟶wf 6488  –1-1→wf1 6489  –onto→wfo 6490  –1-1-onto→wf1o 6491   ≼ cdom 8881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-dom 8885

This theorem is referenced by:  cnvct  8971  xpdom3  9003  domunsncan  9005  domtriord  9051  sdomel  9052  sdomdif  9053  onsdominel  9054  pwdom  9057  2pwuninel  9060  mapdom1  9070  mapdom3  9077  limenpsi  9080  unbnn  9196  fodomfiOLD  9230  fidomdm  9234  hartogslem1  9447  hartogs  9449  card2on  9459  wdompwdom  9483  wdom2d  9485  wdomima2g  9491  unxpwdom2  9493  unxpwdom  9494  harwdom  9496  r1sdom  9686  tskwe  9862  carddomi2  9882  cardsdomelir  9885  cardsdomel  9886  harcard  9890  carduni  9893  cardmin2  9911  infxpenlem  9923  ssnum  9949  acnnum  9962  fodomfi2  9970  inffien  9973  alephordi  9984  dfac12lem2  10055  djudoml  10095  cdainflem  10098  djuinf  10099  unctb  10114  infunabs  10116  infdju  10117  infdif  10118  infdif2  10119  infmap2  10127  ackbij2  10152  fictb  10154  cfslb  10176  fincssdom  10233  fin67  10305  fin1a2lem12  10321  axcclem  10367  dmct  10434  brdom3  10438  brdom5  10439  brdom4  10440  imadomg  10444  fnct  10447  mptct  10448  ondomon  10473  alephval2  10483  alephadd  10488  alephmul  10489  alephexp1  10490  alephsuc3  10491  alephexp2  10492  alephreg  10493  pwcfsdom  10494  cfpwsdom  10495  canthnum  10560  pwfseqlem5  10574  pwxpndom2  10576  pwdjundom  10578  gchaleph  10582  gchaleph2  10583  gchac  10592  winainflem  10604  gchina  10610  tsksdom  10667  tskinf  10680  inttsk  10685  inar1  10686  inatsk  10689  tskord  10691  tskcard  10692  grudomon  10728  gruina  10729  axgroth2  10736  axgroth6  10739  grothac  10741  hashun2  14306  hashss  14332  hashsslei  14349  isercoll  15591  o1fsum  15736  incexc2  15761  znnen  16137  qnnen  16138  rpnnen  16152  ruc  16168  phicl2  16695  phibnd  16698  4sqlem11  16883  vdwlem11  16919  0ram  16948  mreexdomd  17572  pgpssslw  19543  fislw  19554  cctop  22950  1stcfb  23389  2ndc1stc  23395  1stcrestlem  23396  2ndcctbss  23399  2ndcdisj2  23401  2ndcsep  23403  dis2ndc  23404  csdfil  23838  ufilen  23874  opnreen  24776  rectbntr0  24777  ovolctb2  25449  uniiccdif  25535  dyadmbl  25557  opnmblALT  25560  vitali  25570  mbfimaopnlem  25612  mbfsup  25621  fta1blem  26132  aannenlem3  26294  ppiwordi  27128  musum  27157  ppiub  27171  chpub  27187  dirith2  27495  upgrex  29165  rabfodom  32580  abrexdomjm  32582  mptctf  32795  locfinreflem  33997  esumcst  34220  omsmeas  34480  sibfof  34497  subfaclefac  35370  erdszelem10  35394  snmlff  35523  finminlem  36512  iccioo01  37532  isinf2  37610  pibt2  37622  phpreu  37805  lindsdom  37815  poimirlem26  37847  mblfinlem1  37858  abrexdom  37931  heiborlem3  38014  ctbnfien  43060  pellexlem4  43074  pellexlem5  43075  ttac  43278  idomodle  43433  idomsubgmo  43435  iscard5  43777  modelaxreplem1  45219  uzct  45308  rn1st  45517  smfaddlem2  47008  smfmullem4  47038  smfpimbor1lem1  47042  aacllem  50046