![]() |
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 5328 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
2 | simpr 484 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) | |
3 | f1oi 6886 | . . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
4 | dff1o3 6854 | . . . . . . . . 9 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴))) | |
5 | 3, 4 | mpbi 230 | . . . . . . . 8 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 ∧ Fun ◡( I ↾ 𝐴)) |
6 | 5 | simpli 483 | . . . . . . 7 ⊢ ( I ↾ 𝐴):𝐴–onto→𝐴 |
7 | fof 6820 | . . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴) | |
8 | 6, 7 | ax-mp 5 | . . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴 |
9 | fss 6752 | . . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵) | |
10 | 8, 9 | mpan 690 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵) |
11 | funi 6599 | . . . . . . 7 ⊢ Fun I | |
12 | cnvi 6163 | . . . . . . . 8 ⊢ ◡ I = I | |
13 | 12 | funeqi 6588 | . . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I ) |
14 | 11, 13 | mpbir 231 | . . . . . 6 ⊢ Fun ◡ I |
15 | funres11 6644 | . . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴)) | |
16 | 14, 15 | ax-mp 5 | . . . . 5 ⊢ Fun ◡( I ↾ 𝐴) |
17 | df-f1 6567 | . . . . 5 ⊢ (( I ↾ 𝐴):𝐴–1-1→𝐵 ↔ (( I ↾ 𝐴):𝐴⟶𝐵 ∧ Fun ◡( I ↾ 𝐴))) | |
18 | 10, 16, 17 | sylanblrc 590 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
19 | 18 | adantr 480 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → ( I ↾ 𝐴):𝐴–1-1→𝐵) |
20 | f1dom2g 9008 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | |
21 | 1, 2, 19, 20 | syl3anc 1370 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵) |
22 | 21 | expcom 413 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2105 Vcvv 3477 ⊆ wss 3962 class class class wbr 5147 I cid 5581 ◡ccnv 5687 ↾ cres 5690 Fun wfun 6556 ⟶wf 6558 –1-1→wf1 6559 –onto→wfo 6560 –1-1-onto→wf1o 6561 ≼ cdom 8981 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-dom 8985 |
This theorem is referenced by: cnvct 9072 ssctOLD 9090 undomOLD 9098 xpdom3 9108 domunsncan 9110 sucdom2OLD 9120 0domgOLD 9139 domtriord 9161 sdomel 9162 sdomdif 9163 onsdominel 9164 pwdom 9167 2pwuninel 9170 mapdom1 9180 mapdom3 9187 limenpsi 9190 phpOLD 9256 php2OLD 9257 php3OLD 9258 nndomogOLD 9260 onomeneqOLD 9263 unbnn 9329 nnsdomgOLD 9333 fodomfiOLD 9367 fidomdm 9371 hartogslem1 9579 hartogs 9581 card2on 9591 wdompwdom 9615 wdom2d 9617 wdomima2g 9623 unxpwdom2 9625 unxpwdom 9626 harwdom 9628 r1sdom 9811 tskwe 9987 carddomi2 10007 cardsdomelir 10010 cardsdomel 10011 harcard 10015 carduni 10018 cardmin2 10036 infxpenlem 10050 ssnum 10076 acnnum 10089 fodomfi2 10097 inffien 10100 alephordi 10111 dfac12lem2 10182 djudoml 10222 cdainflem 10225 djuinf 10226 unctb 10241 infunabs 10243 infdju 10244 infdif 10245 infdif2 10246 infmap2 10254 ackbij2 10279 fictb 10281 cfslb 10303 fincssdom 10360 fin67 10432 fin1a2lem12 10448 axcclem 10494 dmct 10561 brdom3 10565 brdom5 10566 brdom4 10567 imadomg 10571 fnct 10574 mptct 10575 ondomon 10600 alephval2 10609 alephadd 10614 alephmul 10615 alephexp1 10616 alephsuc3 10617 alephexp2 10618 alephreg 10619 pwcfsdom 10620 cfpwsdom 10621 canthnum 10686 pwfseqlem5 10700 pwxpndom2 10702 pwdjundom 10704 gchaleph 10708 gchaleph2 10709 gchac 10718 winainflem 10730 gchina 10736 tsksdom 10793 tskinf 10806 inttsk 10811 inar1 10812 inatsk 10815 tskord 10817 tskcard 10818 grudomon 10854 gruina 10855 axgroth2 10862 axgroth6 10865 grothac 10867 hashun2 14418 hashss 14444 hashsslei 14461 isercoll 15700 o1fsum 15845 incexc2 15870 znnen 16244 qnnen 16245 rpnnen 16259 ruc 16275 phicl2 16801 phibnd 16804 4sqlem11 16988 vdwlem11 17024 0ram 17053 mreexdomd 17693 pgpssslw 19646 fislw 19657 cctop 23028 1stcfb 23468 2ndc1stc 23474 1stcrestlem 23475 2ndcctbss 23478 2ndcdisj2 23480 2ndcsep 23482 dis2ndc 23483 csdfil 23917 ufilen 23953 opnreen 24866 rectbntr0 24867 ovolctb2 25540 uniiccdif 25626 dyadmbl 25648 opnmblALT 25651 vitali 25661 mbfimaopnlem 25703 mbfsup 25712 fta1blem 26224 aannenlem3 26386 ppiwordi 27219 musum 27248 ppiub 27262 chpub 27278 dirith2 27586 upgrex 29123 rabfodom 32532 abrexdomjm 32534 mptctf 32734 locfinreflem 33800 esumcst 34043 omsmeas 34304 sibfof 34321 subfaclefac 35160 erdszelem10 35184 snmlff 35313 finminlem 36300 iccioo01 37309 isinf2 37387 pibt2 37399 phpreu 37590 lindsdom 37600 poimirlem26 37632 mblfinlem1 37643 abrexdom 37716 heiborlem3 37799 ctbnfien 42805 pellexlem4 42819 pellexlem5 42820 ttac 43024 idomodle 43179 idomsubgmo 43181 iscard5 43525 modelaxreplem1 44942 uzct 45002 rn1st 45218 smfaddlem2 46719 smfmullem4 46749 smfpimbor1lem1 46753 aacllem 49031 |
Copyright terms: Public domain | W3C validator |