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 4732 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
2 | simpr 476 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) | |
3 | f1oi 6086 | . . . . . . . . . 10 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
4 | dff1o3 6056 | . . . . . . . . . 10 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))) | |
5 | 3, 4 | mpbi 219 | . . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)) |
6 | 5 | simpli 473 | . . . . . . . 8 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴 |
7 | fof 6028 | . . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴) | |
8 | 6, 7 | ax-mp 5 | . . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴 |
9 | fss 5969 | . . . . . . 7 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵) | |
10 | 8, 9 | mpan 702 | . . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵) |
11 | funi 5834 | . . . . . . . 8 ⊢ Fun I | |
12 | cnvi 5456 | . . . . . . . . 9 ⊢ ◡ I = I | |
13 | 12 | funeqi 5824 | . . . . . . . 8 ⊢ (Fun ◡ I ↔ Fun I ) |
14 | 11, 13 | mpbir 220 | . . . . . . 7 ⊢ Fun ◡ I |
15 | funres11 5880 | . . . . . . 7 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴)) | |
16 | 14, 15 | ax-mp 5 | . . . . . 6 ⊢ Fun ◡( I ↾ 𝐴) |
17 | 10, 16 | jctir 559 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴))) |
18 | df-f1 5809 | . . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴))) | |
19 | 17, 18 | sylibr 223 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
20 | 19 | adantr 480 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
21 | f1dom2g 7859 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | |
22 | 1, 2, 20, 21 | syl3anc 1318 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵) |
23 | 22 | expcom 450 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 1977 Vcvv 3173 ⊆ wss 3540 class class class wbr 4583 I cid 4948 ◡ccnv 5037 ↾ cres 5040 Fun wfun 5798 ⟶wf 5800 –1-1→wf1 5801 –onto→wfo 5802 –1-1-onto→wf1o 5803 ≼ cdom 7839 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-dom 7843 |
This theorem is referenced by: ssct 7926 undom 7933 xpdom3 7943 domunsncan 7945 0domg 7972 domtriord 7991 sdomel 7992 sdomdif 7993 onsdominel 7994 pwdom 7997 2pwuninel 8000 mapdom1 8010 mapdom3 8017 limenpsi 8020 php 8029 php2 8030 php3 8031 onomeneq 8035 nndomo 8039 sucdom2 8041 unbnn 8101 nnsdomg 8104 fodomfi 8124 fidomdm 8128 pwfilem 8143 hartogslem1 8330 hartogs 8332 card2on 8342 wdompwdom 8366 wdom2d 8368 wdomima2g 8374 unxpwdom2 8376 unxpwdom 8377 harwdom 8378 r1sdom 8520 tskwe 8659 carddomi2 8679 cardsdomelir 8682 cardsdomel 8683 harcard 8687 carduni 8690 cardmin2 8707 infxpenlem 8719 ssnum 8745 acnnum 8758 fodomfi2 8766 inffien 8769 alephordi 8780 dfac12lem2 8849 cdadom3 8893 cdainflem 8896 cdainf 8897 unctb 8910 infunabs 8912 infcda 8913 infdif 8914 infdif2 8915 infmap2 8923 ackbij2 8948 fictb 8950 cfslb 8971 fincssdom 9028 fin67 9100 fin1a2lem12 9116 axcclem 9162 brdom3 9231 brdom5 9232 brdom4 9233 imadomg 9237 ondomon 9264 alephval2 9273 alephadd 9278 alephmul 9279 alephexp1 9280 alephsuc3 9281 alephexp2 9282 alephreg 9283 pwcfsdom 9284 cfpwsdom 9285 canthnum 9350 pwfseqlem5 9364 pwxpndom2 9366 pwcdandom 9368 gchaleph 9372 gchaleph2 9373 gchac 9382 winainflem 9394 gchina 9400 tsksdom 9457 tskinf 9470 inttsk 9475 inar1 9476 inatsk 9479 tskord 9481 tskcard 9482 grudomon 9518 gruina 9519 axgroth2 9526 axgroth6 9529 grothac 9531 hashun2 13033 hashss 13058 hashsslei 13073 isercoll 14246 o1fsum 14386 incexc2 14409 znnen 14780 qnnen 14781 rpnnen 14795 ruc 14811 phicl2 15311 phibnd 15314 4sqlem11 15497 vdwlem11 15533 0ram 15562 mreexdomd 16133 pgpssslw 17852 fislw 17863 cctop 20620 1stcfb 21058 2ndc1stc 21064 1stcrestlem 21065 2ndcctbss 21068 2ndcdisj2 21070 2ndcsep 21072 dis2ndc 21073 csdfil 21508 ufilen 21544 opnreen 22442 rectbntr0 22443 ovolctb2 23067 uniiccdif 23152 dyadmbl 23174 opnmblALT 23177 vitali 23188 mbfimaopnlem 23228 mbfsup 23237 fta1blem 23732 aannenlem3 23889 ppiwordi 24688 musum 24717 ppiub 24729 chpub 24745 dchrisum0re 25002 dirith2 25017 upgrex 25759 umgraex 25852 konigsberg 26514 rabfodom 28728 abrexdomjm 28729 fnct 28876 dmct 28877 cnvct 28878 mptct 28880 mptctf 28883 locfinreflem 29235 esumcst 29452 omsmeas 29712 sibfof 29729 subfaclefac 30412 erdszelem10 30436 snmlff 30565 finminlem 31482 phpreu 32563 lindsdom 32573 poimirlem26 32605 mblfinlem1 32616 abrexdom 32695 heiborlem3 32782 ctbnfien 36400 pellexlem4 36414 pellexlem5 36415 ttac 36621 idomodle 36793 idomsubgmo 36795 uzct 38257 smfaddlem2 39650 smfmullem4 39679 smfpimbor1lem1 39683 aacllem 42356 |
Copyright terms: Public domain | W3C validator |