Theorem ssdomg 9040

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 5323	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6886	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6854	. . . . . . . . 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 6820	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6752	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 690	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6598	. . . . . . 7 ⊢ Fun I
12		cnvi 6161	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6587	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 231	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6643	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6566	. . . . 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 9010	. . 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 2108  Vcvv 3480   ⊆ wss 3951   class class class wbr 5143   I cid 5577  ^◡ccnv 5684   ↾ cres 5687  Fun wfun 6555  ⟶wf 6557  –1-1→wf1 6558  –onto→wfo 6559  –1-1-onto→wf1o 6560   ≼ cdom 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-dom 8987

This theorem is referenced by:  cnvct  9074  ssctOLD  9092  undomOLD  9100  xpdom3  9110  domunsncan  9112  sucdom2OLD  9122  0domgOLD  9141  domtriord  9163  sdomel  9164  sdomdif  9165  onsdominel  9166  pwdom  9169  2pwuninel  9172  mapdom1  9182  mapdom3  9189  limenpsi  9192  phpOLD  9259  php2OLD  9260  php3OLD  9261  nndomogOLD  9263  onomeneqOLD  9266  unbnn  9332  nnsdomgOLD  9336  fodomfiOLD  9370  fidomdm  9374  hartogslem1  9582  hartogs  9584  card2on  9594  wdompwdom  9618  wdom2d  9620  wdomima2g  9626  unxpwdom2  9628  unxpwdom  9629  harwdom  9631  r1sdom  9814  tskwe  9990  carddomi2  10010  cardsdomelir  10013  cardsdomel  10014  harcard  10018  carduni  10021  cardmin2  10039  infxpenlem  10053  ssnum  10079  acnnum  10092  fodomfi2  10100  inffien  10103  alephordi  10114  dfac12lem2  10185  djudoml  10225  cdainflem  10228  djuinf  10229  unctb  10244  infunabs  10246  infdju  10247  infdif  10248  infdif2  10249  infmap2  10257  ackbij2  10282  fictb  10284  cfslb  10306  fincssdom  10363  fin67  10435  fin1a2lem12  10451  axcclem  10497  dmct  10564  brdom3  10568  brdom5  10569  brdom4  10570  imadomg  10574  fnct  10577  mptct  10578  ondomon  10603  alephval2  10612  alephadd  10617  alephmul  10618  alephexp1  10619  alephsuc3  10620  alephexp2  10621  alephreg  10622  pwcfsdom  10623  cfpwsdom  10624  canthnum  10689  pwfseqlem5  10703  pwxpndom2  10705  pwdjundom  10707  gchaleph  10711  gchaleph2  10712  gchac  10721  winainflem  10733  gchina  10739  tsksdom  10796  tskinf  10809  inttsk  10814  inar1  10815  inatsk  10818  tskord  10820  tskcard  10821  grudomon  10857  gruina  10858  axgroth2  10865  axgroth6  10868  grothac  10870  hashun2  14422  hashss  14448  hashsslei  14465  isercoll  15704  o1fsum  15849  incexc2  15874  znnen  16248  qnnen  16249  rpnnen  16263  ruc  16279  phicl2  16805  phibnd  16808  4sqlem11  16993  vdwlem11  17029  0ram  17058  mreexdomd  17692  pgpssslw  19632  fislw  19643  cctop  23013  1stcfb  23453  2ndc1stc  23459  1stcrestlem  23460  2ndcctbss  23463  2ndcdisj2  23465  2ndcsep  23467  dis2ndc  23468  csdfil  23902  ufilen  23938  opnreen  24853  rectbntr0  24854  ovolctb2  25527  uniiccdif  25613  dyadmbl  25635  opnmblALT  25638  vitali  25648  mbfimaopnlem  25690  mbfsup  25699  fta1blem  26210  aannenlem3  26372  ppiwordi  27205  musum  27234  ppiub  27248  chpub  27264  dirith2  27572  upgrex  29109  rabfodom  32524  abrexdomjm  32526  mptctf  32729  locfinreflem  33839  esumcst  34064  omsmeas  34325  sibfof  34342  subfaclefac  35181  erdszelem10  35205  snmlff  35334  finminlem  36319  iccioo01  37328  isinf2  37406  pibt2  37418  phpreu  37611  lindsdom  37621  poimirlem26  37653  mblfinlem1  37664  abrexdom  37737  heiborlem3  37820  ctbnfien  42829  pellexlem4  42843  pellexlem5  42844  ttac  43048  idomodle  43203  idomsubgmo  43205  iscard5  43549  modelaxreplem1  44995  uzct  45068  rn1st  45280  smfaddlem2  46779  smfmullem4  46809  smfpimbor1lem1  46813  aacllem  49320