Theorem ssdomg 8786

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 5247	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V)
2		simpr 485	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
3		f1oi 6754	. . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
4		dff1o3 6722	. . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)))
5	3, 4	mpbi 229	. . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))
6	5	simpli 484	. . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴
7		fof 6688	. . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴)
8	6, 7	ax-mp 5	. . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴
9		fss 6617	. . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵)
10	8, 9	mpan 687	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵)
11		funi 6466	. . . . . . 7 ⊢ Fun I
12		cnvi 6045	. . . . . . . 8 ⊢ ◡ I = I
13	12	funeqi 6455	. . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I )
14	11, 13	mpbir 230	. . . . . 6 ⊢ Fun ◡ I
15		funres11 6511	. . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴))
16	14, 15	ax-mp 5	. . . . 5 ⊢ Fun ◡( I ↾ 𝐴)
17		df-f1 6438	. . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴)))
18	10, 16, 17	sylanblrc 590	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵)
19	18	adantr 481	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵)
20		f1dom2g 8757	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
21	1, 2, 19, 20	syl3anc 1370	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵)
22	21	expcom 414	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3432   ⊆ wss 3887   class class class wbr 5074   I cid 5488  ^◡ccnv 5588   ↾ cres 5591  Fun wfun 6427  ⟶wf 6429  –1-1→wf1 6430  –onto→wfo 6431  –1-1-onto→wf1o 6432   ≼ cdom 8731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-dom 8735

This theorem is referenced by:  cnvct  8824  ssct  8839  undomOLD  8847  xpdom3  8857  domunsncan  8859  sucdom2OLD  8869  0domgOLD  8888  domtriord  8910  sdomel  8911  sdomdif  8912  onsdominel  8913  pwdom  8916  2pwuninel  8919  mapdom1  8929  mapdom3  8936  limenpsi  8939  phpOLD  9005  php2OLD  9006  php3OLD  9007  nndomogOLD  9009  onomeneqOLD  9012  unbnn  9070  nnsdomg  9073  fodomfi  9092  fidomdm  9096  pwfilemOLD  9113  hartogslem1  9301  hartogs  9303  card2on  9313  wdompwdom  9337  wdom2d  9339  wdomima2g  9345  unxpwdom2  9347  unxpwdom  9348  harwdom  9350  r1sdom  9532  tskwe  9708  carddomi2  9728  cardsdomelir  9731  cardsdomel  9732  harcard  9736  carduni  9739  cardmin2  9757  infxpenlem  9769  ssnum  9795  acnnum  9808  fodomfi2  9816  inffien  9819  alephordi  9830  dfac12lem2  9900  djudoml  9940  cdainflem  9943  djuinf  9944  unctb  9961  infunabs  9963  infdju  9964  infdif  9965  infdif2  9966  infmap2  9974  ackbij2  9999  fictb  10001  cfslb  10022  fincssdom  10079  fin67  10151  fin1a2lem12  10167  axcclem  10213  dmct  10280  brdom3  10284  brdom5  10285  brdom4  10286  imadomg  10290  fnct  10293  mptct  10294  ondomon  10319  alephval2  10328  alephadd  10333  alephmul  10334  alephexp1  10335  alephsuc3  10336  alephexp2  10337  alephreg  10338  pwcfsdom  10339  cfpwsdom  10340  canthnum  10405  pwfseqlem5  10419  pwxpndom2  10421  pwdjundom  10423  gchaleph  10427  gchaleph2  10428  gchac  10437  winainflem  10449  gchina  10455  tsksdom  10512  tskinf  10525  inttsk  10530  inar1  10531  inatsk  10534  tskord  10536  tskcard  10537  grudomon  10573  gruina  10574  axgroth2  10581  axgroth6  10584  grothac  10586  hashun2  14098  hashss  14124  hashsslei  14141  isercoll  15379  o1fsum  15525  incexc2  15550  znnen  15921  qnnen  15922  rpnnen  15936  ruc  15952  phicl2  16469  phibnd  16472  4sqlem11  16656  vdwlem11  16692  0ram  16721  mreexdomd  17358  pgpssslw  19219  fislw  19230  cctop  22156  1stcfb  22596  2ndc1stc  22602  1stcrestlem  22603  2ndcctbss  22606  2ndcdisj2  22608  2ndcsep  22610  dis2ndc  22611  csdfil  23045  ufilen  23081  opnreen  23994  rectbntr0  23995  ovolctb2  24656  uniiccdif  24742  dyadmbl  24764  opnmblALT  24767  vitali  24777  mbfimaopnlem  24819  mbfsup  24828  fta1blem  25333  aannenlem3  25490  ppiwordi  26311  musum  26340  ppiub  26352  chpub  26368  dirith2  26676  upgrex  27462  rabfodom  30851  abrexdomjm  30852  mptctf  31052  locfinreflem  31790  esumcst  32031  omsmeas  32290  sibfof  32307  subfaclefac  33138  erdszelem10  33162  snmlff  33291  finminlem  34507  iccioo01  35498  isinf2  35576  pibt2  35588  phpreu  35761  lindsdom  35771  poimirlem26  35803  mblfinlem1  35814  abrexdom  35888  heiborlem3  35971  ctbnfien  40640  pellexlem4  40654  pellexlem5  40655  ttac  40858  idomodle  41021  idomsubgmo  41023  iscard5  41143  uzct  42611  smfaddlem2  44299  smfmullem4  44328  smfpimbor1lem1  44332  aacllem  46505