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 5220 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
2 | simpr 487 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) | |
3 | f1oi 6647 | . . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
4 | dff1o3 6616 | . . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))) | |
5 | 3, 4 | mpbi 232 | . . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)) |
6 | 5 | simpli 486 | . . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴 |
7 | fof 6585 | . . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴) | |
8 | 6, 7 | ax-mp 5 | . . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴 |
9 | fss 6522 | . . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵) | |
10 | 8, 9 | mpan 688 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵) |
11 | funi 6382 | . . . . . . 7 ⊢ Fun I | |
12 | cnvi 5995 | . . . . . . . 8 ⊢ ◡ I = I | |
13 | 12 | funeqi 6371 | . . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I ) |
14 | 11, 13 | mpbir 233 | . . . . . 6 ⊢ Fun ◡ I |
15 | funres11 6426 | . . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴)) | |
16 | 14, 15 | ax-mp 5 | . . . . 5 ⊢ Fun ◡( I ↾ 𝐴) |
17 | df-f1 6355 | . . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴))) | |
18 | 10, 16, 17 | sylanblrc 592 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
19 | 18 | adantr 483 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
20 | f1dom2g 8521 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | |
21 | 1, 2, 19, 20 | syl3anc 1367 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵) |
22 | 21 | expcom 416 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2110 Vcvv 3495 ⊆ wss 3936 class class class wbr 5059 I cid 5454 ◡ccnv 5549 ↾ cres 5552 Fun wfun 6344 ⟶wf 6346 –1-1→wf1 6347 –onto→wfo 6348 –1-1-onto→wf1o 6349 ≼ cdom 8501 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4833 df-br 5060 df-opab 5122 df-id 5455 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-dom 8505 |
This theorem is referenced by: cnvct 8580 ssct 8592 undom 8599 xpdom3 8609 domunsncan 8611 0domg 8638 domtriord 8657 sdomel 8658 sdomdif 8659 onsdominel 8660 pwdom 8663 2pwuninel 8666 mapdom1 8676 mapdom3 8683 limenpsi 8686 php 8695 php2 8696 php3 8697 onomeneq 8702 nndomo 8706 sucdom2 8708 unbnn 8768 nnsdomg 8771 fodomfi 8791 fidomdm 8795 pwfilem 8812 hartogslem1 9000 hartogs 9002 card2on 9012 wdompwdom 9036 wdom2d 9038 wdomima2g 9044 unxpwdom2 9046 unxpwdom 9047 harwdom 9048 r1sdom 9197 tskwe 9373 carddomi2 9393 cardsdomelir 9396 cardsdomel 9397 harcard 9401 carduni 9404 cardmin2 9421 infxpenlem 9433 ssnum 9459 acnnum 9472 fodomfi2 9480 inffien 9483 alephordi 9494 dfac12lem2 9564 djudoml 9604 cdainflem 9607 djuinf 9608 unctb 9621 infunabs 9623 infdju 9624 infdif 9625 infdif2 9626 infmap2 9634 ackbij2 9659 fictb 9661 cfslb 9682 fincssdom 9739 fin67 9811 fin1a2lem12 9827 axcclem 9873 dmct 9940 brdom3 9944 brdom5 9945 brdom4 9946 imadomg 9950 fnct 9953 mptct 9954 ondomon 9979 alephval2 9988 alephadd 9993 alephmul 9994 alephexp1 9995 alephsuc3 9996 alephexp2 9997 alephreg 9998 pwcfsdom 9999 cfpwsdom 10000 canthnum 10065 pwfseqlem5 10079 pwxpndom2 10081 pwdjundom 10083 gchaleph 10087 gchaleph2 10088 gchac 10097 winainflem 10109 gchina 10115 tsksdom 10172 tskinf 10185 inttsk 10190 inar1 10191 inatsk 10194 tskord 10196 tskcard 10197 grudomon 10233 gruina 10234 axgroth2 10241 axgroth6 10244 grothac 10246 hashun2 13738 hashss 13764 hashsslei 13781 isercoll 15018 o1fsum 15162 incexc2 15187 znnen 15559 qnnen 15560 rpnnen 15574 ruc 15590 phicl2 16099 phibnd 16102 4sqlem11 16285 vdwlem11 16321 0ram 16350 mreexdomd 16914 pgpssslw 18733 fislw 18744 cctop 21608 1stcfb 22047 2ndc1stc 22053 1stcrestlem 22054 2ndcctbss 22057 2ndcdisj2 22059 2ndcsep 22061 dis2ndc 22062 csdfil 22496 ufilen 22532 opnreen 23433 rectbntr0 23434 ovolctb2 24087 uniiccdif 24173 dyadmbl 24195 opnmblALT 24198 vitali 24208 mbfimaopnlem 24250 mbfsup 24259 fta1blem 24756 aannenlem3 24913 ppiwordi 25733 musum 25762 ppiub 25774 chpub 25790 dirith2 26098 upgrex 26871 rabfodom 30260 abrexdomjm 30261 mptctf 30447 locfinreflem 31099 esumcst 31317 omsmeas 31576 sibfof 31593 subfaclefac 32418 erdszelem10 32442 snmlff 32571 finminlem 33661 isinf2 34680 pibt2 34692 phpreu 34870 lindsdom 34880 poimirlem26 34912 mblfinlem1 34923 abrexdom 34999 heiborlem3 35085 ctbnfien 39408 pellexlem4 39422 pellexlem5 39423 ttac 39626 idomodle 39789 idomsubgmo 39791 nndomog 39890 iscard5 39894 uzct 41318 smfaddlem2 43033 smfmullem4 43062 smfpimbor1lem1 43066 aacllem 44895 |
Copyright terms: Public domain | W3C validator |