![]() |
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 486 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) | |
3 | f1oi 6872 | . . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
4 | dff1o3 6840 | . . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))) | |
5 | 3, 4 | mpbi 229 | . . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)) |
6 | 5 | simpli 485 | . . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴 |
7 | fof 6806 | . . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴) | |
8 | 6, 7 | ax-mp 5 | . . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴 |
9 | fss 6735 | . . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵) | |
10 | 8, 9 | mpan 689 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵) |
11 | funi 6581 | . . . . . . 7 ⊢ Fun I | |
12 | cnvi 6142 | . . . . . . . 8 ⊢ ◡ I = I | |
13 | 12 | funeqi 6570 | . . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I ) |
14 | 11, 13 | mpbir 230 | . . . . . 6 ⊢ Fun ◡ I |
15 | funres11 6626 | . . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴)) | |
16 | 14, 15 | ax-mp 5 | . . . . 5 ⊢ Fun ◡( I ↾ 𝐴) |
17 | df-f1 6549 | . . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴))) | |
18 | 10, 16, 17 | sylanblrc 591 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
19 | 18 | adantr 482 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
20 | f1dom2g 8965 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | |
21 | 1, 2, 19, 20 | syl3anc 1372 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵) |
22 | 21 | expcom 415 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 Vcvv 3475 ⊆ wss 3949 class class class wbr 5149 I cid 5574 ◡ccnv 5676 ↾ cres 5679 Fun wfun 6538 ⟶wf 6540 –1-1→wf1 6541 –onto→wfo 6542 –1-1-onto→wf1o 6543 ≼ cdom 8937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-dom 8941 |
This theorem is referenced by: cnvct 9034 ssctOLD 9052 undomOLD 9060 xpdom3 9070 domunsncan 9072 sucdom2OLD 9082 0domgOLD 9101 domtriord 9123 sdomel 9124 sdomdif 9125 onsdominel 9126 pwdom 9129 2pwuninel 9132 mapdom1 9142 mapdom3 9149 limenpsi 9152 phpOLD 9222 php2OLD 9223 php3OLD 9224 nndomogOLD 9226 onomeneqOLD 9229 unbnn 9299 nnsdomgOLD 9303 fodomfi 9325 fidomdm 9329 pwfilemOLD 9346 hartogslem1 9537 hartogs 9539 card2on 9549 wdompwdom 9573 wdom2d 9575 wdomima2g 9581 unxpwdom2 9583 unxpwdom 9584 harwdom 9586 r1sdom 9769 tskwe 9945 carddomi2 9965 cardsdomelir 9968 cardsdomel 9969 harcard 9973 carduni 9976 cardmin2 9994 infxpenlem 10008 ssnum 10034 acnnum 10047 fodomfi2 10055 inffien 10058 alephordi 10069 dfac12lem2 10139 djudoml 10179 cdainflem 10182 djuinf 10183 unctb 10200 infunabs 10202 infdju 10203 infdif 10204 infdif2 10205 infmap2 10213 ackbij2 10238 fictb 10240 cfslb 10261 fincssdom 10318 fin67 10390 fin1a2lem12 10406 axcclem 10452 dmct 10519 brdom3 10523 brdom5 10524 brdom4 10525 imadomg 10529 fnct 10532 mptct 10533 ondomon 10558 alephval2 10567 alephadd 10572 alephmul 10573 alephexp1 10574 alephsuc3 10575 alephexp2 10576 alephreg 10577 pwcfsdom 10578 cfpwsdom 10579 canthnum 10644 pwfseqlem5 10658 pwxpndom2 10660 pwdjundom 10662 gchaleph 10666 gchaleph2 10667 gchac 10676 winainflem 10688 gchina 10694 tsksdom 10751 tskinf 10764 inttsk 10769 inar1 10770 inatsk 10773 tskord 10775 tskcard 10776 grudomon 10812 gruina 10813 axgroth2 10820 axgroth6 10823 grothac 10825 hashun2 14343 hashss 14369 hashsslei 14386 isercoll 15614 o1fsum 15759 incexc2 15784 znnen 16155 qnnen 16156 rpnnen 16170 ruc 16186 phicl2 16701 phibnd 16704 4sqlem11 16888 vdwlem11 16924 0ram 16953 mreexdomd 17593 pgpssslw 19482 fislw 19493 cctop 22509 1stcfb 22949 2ndc1stc 22955 1stcrestlem 22956 2ndcctbss 22959 2ndcdisj2 22961 2ndcsep 22963 dis2ndc 22964 csdfil 23398 ufilen 23434 opnreen 24347 rectbntr0 24348 ovolctb2 25009 uniiccdif 25095 dyadmbl 25117 opnmblALT 25120 vitali 25130 mbfimaopnlem 25172 mbfsup 25181 fta1blem 25686 aannenlem3 25843 ppiwordi 26666 musum 26695 ppiub 26707 chpub 26723 dirith2 27031 upgrex 28352 rabfodom 31743 abrexdomjm 31744 mptctf 31942 locfinreflem 32820 esumcst 33061 omsmeas 33322 sibfof 33339 subfaclefac 34167 erdszelem10 34191 snmlff 34320 finminlem 35203 iccioo01 36208 isinf2 36286 pibt2 36298 phpreu 36472 lindsdom 36482 poimirlem26 36514 mblfinlem1 36525 abrexdom 36598 heiborlem3 36681 ctbnfien 41556 pellexlem4 41570 pellexlem5 41571 ttac 41775 idomodle 41938 idomsubgmo 41940 iscard5 42287 uzct 43750 rn1st 43978 smfaddlem2 45480 smfmullem4 45510 smfpimbor1lem1 45514 aacllem 47848 |
Copyright terms: Public domain | W3C validator |