![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssdomg | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
ssdomg | ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssexg 5041 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
2 | simpr 479 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) | |
3 | f1oi 6428 | . . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
4 | dff1o3 6397 | . . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))) | |
5 | 3, 4 | mpbi 222 | . . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)) |
6 | 5 | simpli 478 | . . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴 |
7 | fof 6366 | . . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴) | |
8 | 6, 7 | ax-mp 5 | . . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴 |
9 | fss 6304 | . . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵) | |
10 | 8, 9 | mpan 680 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵) |
11 | funi 6167 | . . . . . . 7 ⊢ Fun I | |
12 | cnvi 5791 | . . . . . . . 8 ⊢ ◡ I = I | |
13 | 12 | funeqi 6156 | . . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I ) |
14 | 11, 13 | mpbir 223 | . . . . . 6 ⊢ Fun ◡ I |
15 | funres11 6211 | . . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴)) | |
16 | 14, 15 | ax-mp 5 | . . . . 5 ⊢ Fun ◡( I ↾ 𝐴) |
17 | df-f1 6140 | . . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴))) | |
18 | 10, 16, 17 | sylanblrc 584 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
19 | 18 | adantr 474 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
20 | f1dom2g 8259 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | |
21 | 1, 2, 19, 20 | syl3anc 1439 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵) |
22 | 21 | expcom 404 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2107 Vcvv 3398 ⊆ wss 3792 class class class wbr 4886 I cid 5260 ◡ccnv 5354 ↾ cres 5357 Fun wfun 6129 ⟶wf 6131 –1-1→wf1 6132 –onto→wfo 6133 –1-1-onto→wf1o 6134 ≼ cdom 8239 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-fun 6137 df-fn 6138 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 df-dom 8243 |
This theorem is referenced by: cnvct 8318 ssct 8329 undom 8336 xpdom3 8346 domunsncan 8348 0domg 8375 domtriord 8394 sdomel 8395 sdomdif 8396 onsdominel 8397 pwdom 8400 2pwuninel 8403 mapdom1 8413 mapdom3 8420 limenpsi 8423 php 8432 php2 8433 php3 8434 onomeneq 8438 nndomo 8442 sucdom2 8444 unbnn 8504 nnsdomg 8507 fodomfi 8527 fidomdm 8531 pwfilem 8548 hartogslem1 8736 hartogs 8738 card2on 8748 wdompwdom 8772 wdom2d 8774 wdomima2g 8780 unxpwdom2 8782 unxpwdom 8783 harwdom 8784 r1sdom 8934 tskwe 9109 carddomi2 9129 cardsdomelir 9132 cardsdomel 9133 harcard 9137 carduni 9140 cardmin2 9157 infxpenlem 9169 ssnum 9195 acnnum 9208 fodomfi2 9216 inffien 9219 alephordi 9230 dfac12lem2 9301 cdadom3 9345 cdainflem 9348 cdainf 9349 unctb 9362 infunabs 9364 infcda 9365 infdif 9366 infdif2 9367 infmap2 9375 ackbij2 9400 fictb 9402 cfslb 9423 fincssdom 9480 fin67 9552 fin1a2lem12 9568 axcclem 9614 dmct 9681 brdom3 9685 brdom5 9686 brdom4 9687 imadomg 9691 fnct 9694 mptct 9695 ondomon 9720 alephval2 9729 alephadd 9734 alephmul 9735 alephexp1 9736 alephsuc3 9737 alephexp2 9738 alephreg 9739 pwcfsdom 9740 cfpwsdom 9741 canthnum 9806 pwfseqlem5 9820 pwxpndom2 9822 pwcdandom 9824 gchaleph 9828 gchaleph2 9829 gchac 9838 winainflem 9850 gchina 9856 tsksdom 9913 tskinf 9926 inttsk 9931 inar1 9932 inatsk 9935 tskord 9937 tskcard 9938 grudomon 9974 gruina 9975 axgroth2 9982 axgroth6 9985 grothac 9987 hashun2 13487 hashss 13511 hashsslei 13527 isercoll 14806 o1fsum 14949 incexc2 14974 znnen 15345 qnnen 15346 rpnnen 15360 ruc 15376 phicl2 15877 phibnd 15880 4sqlem11 16063 vdwlem11 16099 0ram 16128 mreexdomd 16695 pgpssslw 18413 fislw 18424 cctop 21218 1stcfb 21657 2ndc1stc 21663 1stcrestlem 21664 2ndcctbss 21667 2ndcdisj2 21669 2ndcsep 21671 dis2ndc 21672 csdfil 22106 ufilen 22142 opnreen 23042 rectbntr0 23043 ovolctb2 23696 uniiccdif 23782 dyadmbl 23804 opnmblALT 23807 vitali 23817 mbfimaopnlem 23859 mbfsup 23868 fta1blem 24365 aannenlem3 24522 ppiwordi 25340 musum 25369 ppiub 25381 chpub 25397 dchrisum0re 25654 dirith2 25669 upgrex 26440 rabfodom 29906 abrexdomjm 29907 mptctf 30061 locfinreflem 30505 esumcst 30723 omsmeas 30983 sibfof 31000 subfaclefac 31757 erdszelem10 31781 snmlff 31910 finminlem 32901 phpreu 34020 lindsdom 34031 poimirlem26 34063 mblfinlem1 34074 abrexdom 34152 heiborlem3 34238 ctbnfien 38346 pellexlem4 38360 pellexlem5 38361 ttac 38566 idomodle 38737 idomsubgmo 38739 uzct 40167 smfaddlem2 41903 smfmullem4 41932 smfpimbor1lem1 41936 aacllem 43657 |
Copyright terms: Public domain | W3C validator |