| 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 5323 | . . 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 6598 | . . . . . . 7 ⊢ Fun I | |
| 12 | cnvi 6161 | . . . . . . . 8 ⊢ ◡ I = I | |
| 13 | 12 | funeqi 6587 | . . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I ) |
| 14 | 11, 13 | mpbir 231 | . . . . . 6 ⊢ Fun ◡ I |
| 15 | funres11 6643 | . . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴)) | |
| 16 | 14, 15 | ax-mp 5 | . . . . 5 ⊢ Fun ◡( I ↾ 𝐴) |
| 17 | df-f1 6566 | . . . . 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 9010 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | |
| 21 | 1, 2, 19, 20 | syl3anc 1373 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ≼ 𝐵) |
| 22 | 21 | expcom 413 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 Vcvv 3480 ⊆ wss 3951 class class class wbr 5143 I cid 5577 ◡ccnv 5684 ↾ cres 5687 Fun wfun 6555 ⟶wf 6557 –1-1→wf1 6558 –onto→wfo 6559 –1-1-onto→wf1o 6560 ≼ cdom 8983 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-dom 8987 |
| This theorem is referenced by: cnvct 9074 ssctOLD 9092 undomOLD 9100 xpdom3 9110 domunsncan 9112 sucdom2OLD 9122 0domgOLD 9141 domtriord 9163 sdomel 9164 sdomdif 9165 onsdominel 9166 pwdom 9169 2pwuninel 9172 mapdom1 9182 mapdom3 9189 limenpsi 9192 phpOLD 9259 php2OLD 9260 php3OLD 9261 nndomogOLD 9263 onomeneqOLD 9266 unbnn 9332 nnsdomgOLD 9336 fodomfiOLD 9370 fidomdm 9374 hartogslem1 9582 hartogs 9584 card2on 9594 wdompwdom 9618 wdom2d 9620 wdomima2g 9626 unxpwdom2 9628 unxpwdom 9629 harwdom 9631 r1sdom 9814 tskwe 9990 carddomi2 10010 cardsdomelir 10013 cardsdomel 10014 harcard 10018 carduni 10021 cardmin2 10039 infxpenlem 10053 ssnum 10079 acnnum 10092 fodomfi2 10100 inffien 10103 alephordi 10114 dfac12lem2 10185 djudoml 10225 cdainflem 10228 djuinf 10229 unctb 10244 infunabs 10246 infdju 10247 infdif 10248 infdif2 10249 infmap2 10257 ackbij2 10282 fictb 10284 cfslb 10306 fincssdom 10363 fin67 10435 fin1a2lem12 10451 axcclem 10497 dmct 10564 brdom3 10568 brdom5 10569 brdom4 10570 imadomg 10574 fnct 10577 mptct 10578 ondomon 10603 alephval2 10612 alephadd 10617 alephmul 10618 alephexp1 10619 alephsuc3 10620 alephexp2 10621 alephreg 10622 pwcfsdom 10623 cfpwsdom 10624 canthnum 10689 pwfseqlem5 10703 pwxpndom2 10705 pwdjundom 10707 gchaleph 10711 gchaleph2 10712 gchac 10721 winainflem 10733 gchina 10739 tsksdom 10796 tskinf 10809 inttsk 10814 inar1 10815 inatsk 10818 tskord 10820 tskcard 10821 grudomon 10857 gruina 10858 axgroth2 10865 axgroth6 10868 grothac 10870 hashun2 14422 hashss 14448 hashsslei 14465 isercoll 15704 o1fsum 15849 incexc2 15874 znnen 16248 qnnen 16249 rpnnen 16263 ruc 16279 phicl2 16805 phibnd 16808 4sqlem11 16993 vdwlem11 17029 0ram 17058 mreexdomd 17692 pgpssslw 19632 fislw 19643 cctop 23013 1stcfb 23453 2ndc1stc 23459 1stcrestlem 23460 2ndcctbss 23463 2ndcdisj2 23465 2ndcsep 23467 dis2ndc 23468 csdfil 23902 ufilen 23938 opnreen 24853 rectbntr0 24854 ovolctb2 25527 uniiccdif 25613 dyadmbl 25635 opnmblALT 25638 vitali 25648 mbfimaopnlem 25690 mbfsup 25699 fta1blem 26210 aannenlem3 26372 ppiwordi 27205 musum 27234 ppiub 27248 chpub 27264 dirith2 27572 upgrex 29109 rabfodom 32524 abrexdomjm 32526 mptctf 32729 locfinreflem 33839 esumcst 34064 omsmeas 34325 sibfof 34342 subfaclefac 35181 erdszelem10 35205 snmlff 35334 finminlem 36319 iccioo01 37328 isinf2 37406 pibt2 37418 phpreu 37611 lindsdom 37621 poimirlem26 37653 mblfinlem1 37664 abrexdom 37737 heiborlem3 37820 ctbnfien 42829 pellexlem4 42843 pellexlem5 42844 ttac 43048 idomodle 43203 idomsubgmo 43205 iscard5 43549 modelaxreplem1 44995 uzct 45068 rn1st 45280 smfaddlem2 46779 smfmullem4 46809 smfpimbor1lem1 46813 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |