Theorem ssdomg 9021

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 5324	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 483	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6876	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6844	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 229	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 482	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6810	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6739	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 688	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6586	. . . . . . 7 ⊢ Fun I
12		cnvi 6148	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6575	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 230	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6631	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6554	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 588	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 479	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8990	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1368	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 412	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  Vcvv 3461   ⊆ wss 3944   class class class wbr 5149   I cid 5575  ^◡ccnv 5677   ↾ cres 5680  Fun wfun 6543  ⟶wf 6545  –1-1→wf1 6546  –onto→wfo 6547  –1-1-onto→wf1o 6548   ≼ cdom 8962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-dom 8966

This theorem is referenced by:  cnvct  9060  ssctOLD  9080  undomOLD  9088  xpdom3  9098  domunsncan  9100  sucdom2OLD  9110  0domgOLD  9129  domtriord  9151  sdomel  9152  sdomdif  9153  onsdominel  9154  pwdom  9157  2pwuninel  9160  mapdom1  9170  mapdom3  9177  limenpsi  9180  phpOLD  9250  php2OLD  9251  php3OLD  9252  nndomogOLD  9254  onomeneqOLD  9257  unbnn  9327  nnsdomgOLD  9331  fodomfi  9356  fidomdm  9360  pwfilemOLD  9377  hartogslem1  9572  hartogs  9574  card2on  9584  wdompwdom  9608  wdom2d  9610  wdomima2g  9616  unxpwdom2  9618  unxpwdom  9619  harwdom  9621  r1sdom  9804  tskwe  9980  carddomi2  10000  cardsdomelir  10003  cardsdomel  10004  harcard  10008  carduni  10011  cardmin2  10029  infxpenlem  10043  ssnum  10069  acnnum  10082  fodomfi2  10090  inffien  10093  alephordi  10104  dfac12lem2  10174  djudoml  10214  cdainflem  10217  djuinf  10218  unctb  10235  infunabs  10237  infdju  10238  infdif  10239  infdif2  10240  infmap2  10248  ackbij2  10273  fictb  10275  cfslb  10296  fincssdom  10353  fin67  10425  fin1a2lem12  10441  axcclem  10487  dmct  10554  brdom3  10558  brdom5  10559  brdom4  10560  imadomg  10564  fnct  10567  mptct  10568  ondomon  10593  alephval2  10602  alephadd  10607  alephmul  10608  alephexp1  10609  alephsuc3  10610  alephexp2  10611  alephreg  10612  pwcfsdom  10613  cfpwsdom  10614  canthnum  10679  pwfseqlem5  10693  pwxpndom2  10695  pwdjundom  10697  gchaleph  10701  gchaleph2  10702  gchac  10711  winainflem  10723  gchina  10729  tsksdom  10786  tskinf  10799  inttsk  10804  inar1  10805  inatsk  10808  tskord  10810  tskcard  10811  grudomon  10847  gruina  10848  axgroth2  10855  axgroth6  10858  grothac  10860  hashun2  14386  hashss  14412  hashsslei  14429  isercoll  15658  o1fsum  15803  incexc2  15828  znnen  16200  qnnen  16201  rpnnen  16215  ruc  16231  phicl2  16756  phibnd  16759  4sqlem11  16943  vdwlem11  16979  0ram  17008  mreexdomd  17648  pgpssslw  19598  fislw  19609  cctop  22970  1stcfb  23410  2ndc1stc  23416  1stcrestlem  23417  2ndcctbss  23420  2ndcdisj2  23422  2ndcsep  23424  dis2ndc  23425  csdfil  23859  ufilen  23895  opnreen  24808  rectbntr0  24809  ovolctb2  25482  uniiccdif  25568  dyadmbl  25590  opnmblALT  25593  vitali  25603  mbfimaopnlem  25645  mbfsup  25654  fta1blem  26167  aannenlem3  26327  ppiwordi  27159  musum  27188  ppiub  27202  chpub  27218  dirith2  27526  upgrex  28997  rabfodom  32399  abrexdomjm  32400  mptctf  32601  locfinreflem  33592  esumcst  33833  omsmeas  34094  sibfof  34111  subfaclefac  34937  erdszelem10  34961  snmlff  35090  finminlem  35953  iccioo01  36957  isinf2  37035  pibt2  37047  phpreu  37228  lindsdom  37238  poimirlem26  37270  mblfinlem1  37281  abrexdom  37354  heiborlem3  37437  ctbnfien  42385  pellexlem4  42399  pellexlem5  42400  ttac  42604  idomodle  42766  idomsubgmo  42768  iscard5  43113  uzct  44574  rn1st  44793  smfaddlem2  46295  smfmullem4  46325  smfpimbor1lem1  46329  aacllem  48425