Theorem ssdomg 8549

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 5220	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 487	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6647	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6616	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 232	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 486	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6585	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6522	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 688	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6382	. . . . . . 7 ⊢ Fun I
12		cnvi 5995	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6371	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 233	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6426	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6355	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 592	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 483	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8521	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1367	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 416	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  Vcvv 3495   ⊆ wss 3936   class class class wbr 5059   I cid 5454  ^◡ccnv 5549   ↾ cres 5552  Fun wfun 6344  ⟶wf 6346  –1-1→wf1 6347  –onto→wfo 6348  –1-1-onto→wf1o 6349   ≼ cdom 8501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-dom 8505

This theorem is referenced by:  cnvct  8580  ssct  8592  undom  8599  xpdom3  8609  domunsncan  8611  0domg  8638  domtriord  8657  sdomel  8658  sdomdif  8659  onsdominel  8660  pwdom  8663  2pwuninel  8666  mapdom1  8676  mapdom3  8683  limenpsi  8686  php  8695  php2  8696  php3  8697  onomeneq  8702  nndomo  8706  sucdom2  8708  unbnn  8768  nnsdomg  8771  fodomfi  8791  fidomdm  8795  pwfilem  8812  hartogslem1  9000  hartogs  9002  card2on  9012  wdompwdom  9036  wdom2d  9038  wdomima2g  9044  unxpwdom2  9046  unxpwdom  9047  harwdom  9048  r1sdom  9197  tskwe  9373  carddomi2  9393  cardsdomelir  9396  cardsdomel  9397  harcard  9401  carduni  9404  cardmin2  9421  infxpenlem  9433  ssnum  9459  acnnum  9472  fodomfi2  9480  inffien  9483  alephordi  9494  dfac12lem2  9564  djudoml  9604  cdainflem  9607  djuinf  9608  unctb  9621  infunabs  9623  infdju  9624  infdif  9625  infdif2  9626  infmap2  9634  ackbij2  9659  fictb  9661  cfslb  9682  fincssdom  9739  fin67  9811  fin1a2lem12  9827  axcclem  9873  dmct  9940  brdom3  9944  brdom5  9945  brdom4  9946  imadomg  9950  fnct  9953  mptct  9954  ondomon  9979  alephval2  9988  alephadd  9993  alephmul  9994  alephexp1  9995  alephsuc3  9996  alephexp2  9997  alephreg  9998  pwcfsdom  9999  cfpwsdom  10000  canthnum  10065  pwfseqlem5  10079  pwxpndom2  10081  pwdjundom  10083  gchaleph  10087  gchaleph2  10088  gchac  10097  winainflem  10109  gchina  10115  tsksdom  10172  tskinf  10185  inttsk  10190  inar1  10191  inatsk  10194  tskord  10196  tskcard  10197  grudomon  10233  gruina  10234  axgroth2  10241  axgroth6  10244  grothac  10246  hashun2  13738  hashss  13764  hashsslei  13781  isercoll  15018  o1fsum  15162  incexc2  15187  znnen  15559  qnnen  15560  rpnnen  15574  ruc  15590  phicl2  16099  phibnd  16102  4sqlem11  16285  vdwlem11  16321  0ram  16350  mreexdomd  16914  pgpssslw  18733  fislw  18744  cctop  21608  1stcfb  22047  2ndc1stc  22053  1stcrestlem  22054  2ndcctbss  22057  2ndcdisj2  22059  2ndcsep  22061  dis2ndc  22062  csdfil  22496  ufilen  22532  opnreen  23433  rectbntr0  23434  ovolctb2  24087  uniiccdif  24173  dyadmbl  24195  opnmblALT  24198  vitali  24208  mbfimaopnlem  24250  mbfsup  24259  fta1blem  24756  aannenlem3  24913  ppiwordi  25733  musum  25762  ppiub  25774  chpub  25790  dirith2  26098  upgrex  26871  rabfodom  30260  abrexdomjm  30261  mptctf  30447  locfinreflem  31099  esumcst  31317  omsmeas  31576  sibfof  31593  subfaclefac  32418  erdszelem10  32442  snmlff  32571  finminlem  33661  isinf2  34680  pibt2  34692  phpreu  34870  lindsdom  34880  poimirlem26  34912  mblfinlem1  34923  abrexdom  34999  heiborlem3  35085  ctbnfien  39408  pellexlem4  39422  pellexlem5  39423  ttac  39626  idomodle  39789  idomsubgmo  39791  nndomog  39890  iscard5  39894  uzct  41318  smfaddlem2  43033  smfmullem4  43062  smfpimbor1lem1  43066  aacllem  44895