ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssdomg GIF version

Theorem ssdomg 6449
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
StepHypRef Expression
1 ssexg 3955 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐴 ∈ V)
2 simpr 108 . . 3 ((𝐴𝐵𝐵𝑉) → 𝐵𝑉)
3 f1oi 5256 . . . . . . . . . 10 ( I ↾ 𝐴):𝐴1-1-onto𝐴
4 dff1o3 5224 . . . . . . . . . 10 (( I ↾ 𝐴):𝐴1-1-onto𝐴 ↔ (( I ↾ 𝐴):𝐴onto𝐴 ∧ Fun ( I ↾ 𝐴)))
53, 4mpbi 143 . . . . . . . . 9 (( I ↾ 𝐴):𝐴onto𝐴 ∧ Fun ( I ↾ 𝐴))
65simpli 109 . . . . . . . 8 ( I ↾ 𝐴):𝐴onto𝐴
7 fof 5198 . . . . . . . 8 (( I ↾ 𝐴):𝐴onto𝐴 → ( I ↾ 𝐴):𝐴𝐴)
86, 7ax-mp 7 . . . . . . 7 ( I ↾ 𝐴):𝐴𝐴
9 fss 5138 . . . . . . 7 ((( I ↾ 𝐴):𝐴𝐴𝐴𝐵) → ( I ↾ 𝐴):𝐴𝐵)
108, 9mpan 415 . . . . . 6 (𝐴𝐵 → ( I ↾ 𝐴):𝐴𝐵)
11 funi 5013 . . . . . . . 8 Fun I
12 cnvi 4804 . . . . . . . . 9 I = I
1312funeqi 5003 . . . . . . . 8 (Fun I ↔ Fun I )
1411, 13mpbir 144 . . . . . . 7 Fun I
15 funres11 5053 . . . . . . 7 (Fun I → Fun ( I ↾ 𝐴))
1614, 15ax-mp 7 . . . . . 6 Fun ( I ↾ 𝐴)
1710, 16jctir 306 . . . . 5 (𝐴𝐵 → (( I ↾ 𝐴):𝐴𝐵 ∧ Fun ( I ↾ 𝐴)))
18 df-f1 4988 . . . . 5 (( I ↾ 𝐴):𝐴1-1𝐵 ↔ (( I ↾ 𝐴):𝐴𝐵 ∧ Fun ( I ↾ 𝐴)))
1917, 18sylibr 132 . . . 4 (𝐴𝐵 → ( I ↾ 𝐴):𝐴1-1𝐵)
2019adantr 270 . . 3 ((𝐴𝐵𝐵𝑉) → ( I ↾ 𝐴):𝐴1-1𝐵)
21 f1dom2g 6427 . . 3 ((𝐴 ∈ V ∧ 𝐵𝑉 ∧ ( I ↾ 𝐴):𝐴1-1𝐵) → 𝐴𝐵)
221, 2, 20, 21syl3anc 1172 . 2 ((𝐴𝐵𝐵𝑉) → 𝐴𝐵)
2322expcom 114 1 (𝐵𝑉 → (𝐴𝐵𝐴𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1436  Vcvv 2615  wss 2988   class class class wbr 3822   I cid 4091  ccnv 4412  cres 4415  Fun wfun 4977  wf 4979  1-1wf1 4980  ontowfo 4981  1-1-ontowf1o 4982  cdom 6410
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-pow 3986  ax-pr 4012  ax-un 4236
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-opab 3877  df-id 4096  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fo 4989  df-f1o 4990  df-dom 6413
This theorem is referenced by:  cnvct  6480  ssct  6488  xpdom3m  6504  0domg  6507  mapdom1g  6517  phplem4dom  6532  nndomo  6534  phpm  6535  fict  6538  domfiexmid  6548  infnfi  6565  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  fihashss  10124  phicl2  11096  phibnd  11099  pw1dom2  11358
  Copyright terms: Public domain W3C validator