![]() |
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 5191 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
2 | simpr 488 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) | |
3 | f1oi 6627 | . . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
4 | dff1o3 6596 | . . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))) | |
5 | 3, 4 | mpbi 233 | . . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)) |
6 | 5 | simpli 487 | . . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴 |
7 | fof 6565 | . . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴) | |
8 | 6, 7 | ax-mp 5 | . . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴 |
9 | fss 6501 | . . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵) | |
10 | 8, 9 | mpan 689 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵) |
11 | funi 6356 | . . . . . . 7 ⊢ Fun I | |
12 | cnvi 5967 | . . . . . . . 8 ⊢ ◡ I = I | |
13 | 12 | funeqi 6345 | . . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I ) |
14 | 11, 13 | mpbir 234 | . . . . . 6 ⊢ Fun ◡ I |
15 | funres11 6401 | . . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴)) | |
16 | 14, 15 | ax-mp 5 | . . . . 5 ⊢ Fun ◡( I ↾ 𝐴) |
17 | df-f1 6329 | . . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴))) | |
18 | 10, 16, 17 | sylanblrc 593 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
19 | 18 | adantr 484 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
20 | f1dom2g 8510 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | |
21 | 1, 2, 19, 20 | syl3anc 1368 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵) |
22 | 21 | expcom 417 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2111 Vcvv 3441 ⊆ wss 3881 class class class wbr 5030 I cid 5424 ◡ccnv 5518 ↾ cres 5521 Fun wfun 6318 ⟶wf 6320 –1-1→wf1 6321 –onto→wfo 6322 –1-1-onto→wf1o 6323 ≼ cdom 8490 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-dom 8494 |
This theorem is referenced by: cnvct 8569 ssct 8581 undom 8588 xpdom3 8598 domunsncan 8600 sucdom2 8610 0domg 8628 domtriord 8647 sdomel 8648 sdomdif 8649 onsdominel 8650 pwdom 8653 2pwuninel 8656 mapdom1 8666 mapdom3 8673 limenpsi 8676 php 8685 php2 8686 php3 8687 nndomog 8692 onomeneq 8693 unbnn 8758 nnsdomg 8761 fodomfi 8781 fidomdm 8785 pwfilem 8802 hartogslem1 8990 hartogs 8992 card2on 9002 wdompwdom 9026 wdom2d 9028 wdomima2g 9034 unxpwdom2 9036 unxpwdom 9037 harwdom 9039 r1sdom 9187 tskwe 9363 carddomi2 9383 cardsdomelir 9386 cardsdomel 9387 harcard 9391 carduni 9394 cardmin2 9412 infxpenlem 9424 ssnum 9450 acnnum 9463 fodomfi2 9471 inffien 9474 alephordi 9485 dfac12lem2 9555 djudoml 9595 cdainflem 9598 djuinf 9599 unctb 9616 infunabs 9618 infdju 9619 infdif 9620 infdif2 9621 infmap2 9629 ackbij2 9654 fictb 9656 cfslb 9677 fincssdom 9734 fin67 9806 fin1a2lem12 9822 axcclem 9868 dmct 9935 brdom3 9939 brdom5 9940 brdom4 9941 imadomg 9945 fnct 9948 mptct 9949 ondomon 9974 alephval2 9983 alephadd 9988 alephmul 9989 alephexp1 9990 alephsuc3 9991 alephexp2 9992 alephreg 9993 pwcfsdom 9994 cfpwsdom 9995 canthnum 10060 pwfseqlem5 10074 pwxpndom2 10076 pwdjundom 10078 gchaleph 10082 gchaleph2 10083 gchac 10092 winainflem 10104 gchina 10110 tsksdom 10167 tskinf 10180 inttsk 10185 inar1 10186 inatsk 10189 tskord 10191 tskcard 10192 grudomon 10228 gruina 10229 axgroth2 10236 axgroth6 10239 grothac 10241 hashun2 13740 hashss 13766 hashsslei 13783 isercoll 15016 o1fsum 15160 incexc2 15185 znnen 15557 qnnen 15558 rpnnen 15572 ruc 15588 phicl2 16095 phibnd 16098 4sqlem11 16281 vdwlem11 16317 0ram 16346 mreexdomd 16912 pgpssslw 18731 fislw 18742 cctop 21611 1stcfb 22050 2ndc1stc 22056 1stcrestlem 22057 2ndcctbss 22060 2ndcdisj2 22062 2ndcsep 22064 dis2ndc 22065 csdfil 22499 ufilen 22535 opnreen 23436 rectbntr0 23437 ovolctb2 24096 uniiccdif 24182 dyadmbl 24204 opnmblALT 24207 vitali 24217 mbfimaopnlem 24259 mbfsup 24268 fta1blem 24769 aannenlem3 24926 ppiwordi 25747 musum 25776 ppiub 25788 chpub 25804 dirith2 26112 upgrex 26885 rabfodom 30274 abrexdomjm 30275 mptctf 30479 locfinreflem 31193 esumcst 31432 omsmeas 31691 sibfof 31708 subfaclefac 32536 erdszelem10 32560 snmlff 32689 finminlem 33779 iccioo01 34741 isinf2 34822 pibt2 34834 phpreu 35041 lindsdom 35051 poimirlem26 35083 mblfinlem1 35094 abrexdom 35168 heiborlem3 35251 ctbnfien 39759 pellexlem4 39773 pellexlem5 39774 ttac 39977 idomodle 40140 idomsubgmo 40142 iscard5 40242 uzct 41697 smfaddlem2 43397 smfmullem4 43426 smfpimbor1lem1 43430 aacllem 45329 |
Copyright terms: Public domain | W3C validator |