![]() |
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 5324 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
2 | simpr 483 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) | |
3 | f1oi 6876 | . . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
4 | dff1o3 6844 | . . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))) | |
5 | 3, 4 | mpbi 229 | . . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)) |
6 | 5 | simpli 482 | . . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴 |
7 | fof 6810 | . . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴) | |
8 | 6, 7 | ax-mp 5 | . . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴 |
9 | fss 6739 | . . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵) | |
10 | 8, 9 | mpan 688 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵) |
11 | funi 6586 | . . . . . . 7 ⊢ Fun I | |
12 | cnvi 6148 | . . . . . . . 8 ⊢ ◡ I = I | |
13 | 12 | funeqi 6575 | . . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I ) |
14 | 11, 13 | mpbir 230 | . . . . . 6 ⊢ Fun ◡ I |
15 | funres11 6631 | . . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴)) | |
16 | 14, 15 | ax-mp 5 | . . . . 5 ⊢ Fun ◡( I ↾ 𝐴) |
17 | df-f1 6554 | . . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴))) | |
18 | 10, 16, 17 | sylanblrc 588 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
19 | 18 | adantr 479 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
20 | f1dom2g 8990 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | |
21 | 1, 2, 19, 20 | syl3anc 1368 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵) |
22 | 21 | expcom 412 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 Vcvv 3461 ⊆ wss 3944 class class class wbr 5149 I cid 5575 ◡ccnv 5677 ↾ cres 5680 Fun wfun 6543 ⟶wf 6545 –1-1→wf1 6546 –onto→wfo 6547 –1-1-onto→wf1o 6548 ≼ cdom 8962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-dom 8966 |
This theorem is referenced by: cnvct 9060 ssctOLD 9080 undomOLD 9088 xpdom3 9098 domunsncan 9100 sucdom2OLD 9110 0domgOLD 9129 domtriord 9151 sdomel 9152 sdomdif 9153 onsdominel 9154 pwdom 9157 2pwuninel 9160 mapdom1 9170 mapdom3 9177 limenpsi 9180 phpOLD 9250 php2OLD 9251 php3OLD 9252 nndomogOLD 9254 onomeneqOLD 9257 unbnn 9327 nnsdomgOLD 9331 fodomfi 9356 fidomdm 9360 pwfilemOLD 9377 hartogslem1 9572 hartogs 9574 card2on 9584 wdompwdom 9608 wdom2d 9610 wdomima2g 9616 unxpwdom2 9618 unxpwdom 9619 harwdom 9621 r1sdom 9804 tskwe 9980 carddomi2 10000 cardsdomelir 10003 cardsdomel 10004 harcard 10008 carduni 10011 cardmin2 10029 infxpenlem 10043 ssnum 10069 acnnum 10082 fodomfi2 10090 inffien 10093 alephordi 10104 dfac12lem2 10174 djudoml 10214 cdainflem 10217 djuinf 10218 unctb 10235 infunabs 10237 infdju 10238 infdif 10239 infdif2 10240 infmap2 10248 ackbij2 10273 fictb 10275 cfslb 10296 fincssdom 10353 fin67 10425 fin1a2lem12 10441 axcclem 10487 dmct 10554 brdom3 10558 brdom5 10559 brdom4 10560 imadomg 10564 fnct 10567 mptct 10568 ondomon 10593 alephval2 10602 alephadd 10607 alephmul 10608 alephexp1 10609 alephsuc3 10610 alephexp2 10611 alephreg 10612 pwcfsdom 10613 cfpwsdom 10614 canthnum 10679 pwfseqlem5 10693 pwxpndom2 10695 pwdjundom 10697 gchaleph 10701 gchaleph2 10702 gchac 10711 winainflem 10723 gchina 10729 tsksdom 10786 tskinf 10799 inttsk 10804 inar1 10805 inatsk 10808 tskord 10810 tskcard 10811 grudomon 10847 gruina 10848 axgroth2 10855 axgroth6 10858 grothac 10860 hashun2 14386 hashss 14412 hashsslei 14429 isercoll 15658 o1fsum 15803 incexc2 15828 znnen 16200 qnnen 16201 rpnnen 16215 ruc 16231 phicl2 16756 phibnd 16759 4sqlem11 16943 vdwlem11 16979 0ram 17008 mreexdomd 17648 pgpssslw 19598 fislw 19609 cctop 22970 1stcfb 23410 2ndc1stc 23416 1stcrestlem 23417 2ndcctbss 23420 2ndcdisj2 23422 2ndcsep 23424 dis2ndc 23425 csdfil 23859 ufilen 23895 opnreen 24808 rectbntr0 24809 ovolctb2 25482 uniiccdif 25568 dyadmbl 25590 opnmblALT 25593 vitali 25603 mbfimaopnlem 25645 mbfsup 25654 fta1blem 26167 aannenlem3 26327 ppiwordi 27159 musum 27188 ppiub 27202 chpub 27218 dirith2 27526 upgrex 28997 rabfodom 32399 abrexdomjm 32400 mptctf 32601 locfinreflem 33592 esumcst 33833 omsmeas 34094 sibfof 34111 subfaclefac 34937 erdszelem10 34961 snmlff 35090 finminlem 35953 iccioo01 36957 isinf2 37035 pibt2 37047 phpreu 37228 lindsdom 37238 poimirlem26 37270 mblfinlem1 37281 abrexdom 37354 heiborlem3 37437 ctbnfien 42385 pellexlem4 42399 pellexlem5 42400 ttac 42604 idomodle 42766 idomsubgmo 42768 iscard5 43113 uzct 44574 rn1st 44793 smfaddlem2 46295 smfmullem4 46325 smfpimbor1lem1 46329 aacllem 48425 |
Copyright terms: Public domain | W3C validator |