![]() |
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 5285 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ V) | |
2 | simpr 486 | . . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) | |
3 | f1oi 6827 | . . . . . . . . 9 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
4 | dff1o3 6795 | . . . . . . . . 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 6761 | . . . . . . 7 ⊢ (( I ↾ 𝐴):𝐴–onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴) | |
8 | 6, 7 | ax-mp 5 | . . . . . 6 ⊢ ( I ↾ 𝐴):𝐴⟶𝐴 |
9 | fss 6690 | . . . . . 6 ⊢ ((( I ↾ 𝐴):𝐴⟶𝐴 ∧ 𝐴 ⊆ 𝐵) → ( I ↾ 𝐴):𝐴⟶𝐵) | |
10 | 8, 9 | mpan 689 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴):𝐴⟶𝐵) |
11 | funi 6538 | . . . . . . 7 ⊢ Fun I | |
12 | cnvi 6099 | . . . . . . . 8 ⊢ ◡ I = I | |
13 | 12 | funeqi 6527 | . . . . . . 7 ⊢ (Fun ◡ I ↔ Fun I ) |
14 | 11, 13 | mpbir 230 | . . . . . 6 ⊢ Fun ◡ I |
15 | funres11 6583 | . . . . . 6 ⊢ (Fun ◡ I → Fun ◡( I ↾ 𝐴)) | |
16 | 14, 15 | ax-mp 5 | . . . . 5 ⊢ Fun ◡( I ↾ 𝐴) |
17 | df-f1 6506 | . . . . 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 8916 | . . 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 3448 ⊆ wss 3915 class class class wbr 5110 I cid 5535 ◡ccnv 5637 ↾ cres 5640 Fun wfun 6495 ⟶wf 6497 –1-1→wf1 6498 –onto→wfo 6499 –1-1-onto→wf1o 6500 ≼ cdom 8888 |
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 2708 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 |
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 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-rex 3075 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-id 5536 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-dom 8892 |
This theorem is referenced by: cnvct 8985 ssctOLD 9003 undomOLD 9011 xpdom3 9021 domunsncan 9023 sucdom2OLD 9033 0domgOLD 9052 domtriord 9074 sdomel 9075 sdomdif 9076 onsdominel 9077 pwdom 9080 2pwuninel 9083 mapdom1 9093 mapdom3 9100 limenpsi 9103 phpOLD 9173 php2OLD 9174 php3OLD 9175 nndomogOLD 9177 onomeneqOLD 9180 unbnn 9250 nnsdomgOLD 9254 fodomfi 9276 fidomdm 9280 pwfilemOLD 9297 hartogslem1 9485 hartogs 9487 card2on 9497 wdompwdom 9521 wdom2d 9523 wdomima2g 9529 unxpwdom2 9531 unxpwdom 9532 harwdom 9534 r1sdom 9717 tskwe 9893 carddomi2 9913 cardsdomelir 9916 cardsdomel 9917 harcard 9921 carduni 9924 cardmin2 9942 infxpenlem 9956 ssnum 9982 acnnum 9995 fodomfi2 10003 inffien 10006 alephordi 10017 dfac12lem2 10087 djudoml 10127 cdainflem 10130 djuinf 10131 unctb 10148 infunabs 10150 infdju 10151 infdif 10152 infdif2 10153 infmap2 10161 ackbij2 10186 fictb 10188 cfslb 10209 fincssdom 10266 fin67 10338 fin1a2lem12 10354 axcclem 10400 dmct 10467 brdom3 10471 brdom5 10472 brdom4 10473 imadomg 10477 fnct 10480 mptct 10481 ondomon 10506 alephval2 10515 alephadd 10520 alephmul 10521 alephexp1 10522 alephsuc3 10523 alephexp2 10524 alephreg 10525 pwcfsdom 10526 cfpwsdom 10527 canthnum 10592 pwfseqlem5 10606 pwxpndom2 10608 pwdjundom 10610 gchaleph 10614 gchaleph2 10615 gchac 10624 winainflem 10636 gchina 10642 tsksdom 10699 tskinf 10712 inttsk 10717 inar1 10718 inatsk 10721 tskord 10723 tskcard 10724 grudomon 10760 gruina 10761 axgroth2 10768 axgroth6 10771 grothac 10773 hashun2 14290 hashss 14316 hashsslei 14333 isercoll 15559 o1fsum 15705 incexc2 15730 znnen 16101 qnnen 16102 rpnnen 16116 ruc 16132 phicl2 16647 phibnd 16650 4sqlem11 16834 vdwlem11 16870 0ram 16899 mreexdomd 17536 pgpssslw 19403 fislw 19414 cctop 22372 1stcfb 22812 2ndc1stc 22818 1stcrestlem 22819 2ndcctbss 22822 2ndcdisj2 22824 2ndcsep 22826 dis2ndc 22827 csdfil 23261 ufilen 23297 opnreen 24210 rectbntr0 24211 ovolctb2 24872 uniiccdif 24958 dyadmbl 24980 opnmblALT 24983 vitali 24993 mbfimaopnlem 25035 mbfsup 25044 fta1blem 25549 aannenlem3 25706 ppiwordi 26527 musum 26556 ppiub 26568 chpub 26584 dirith2 26892 upgrex 28085 rabfodom 31474 abrexdomjm 31475 mptctf 31676 locfinreflem 32461 esumcst 32702 omsmeas 32963 sibfof 32980 subfaclefac 33810 erdszelem10 33834 snmlff 33963 finminlem 34819 iccioo01 35827 isinf2 35905 pibt2 35917 phpreu 36091 lindsdom 36101 poimirlem26 36133 mblfinlem1 36144 abrexdom 36218 heiborlem3 36301 ctbnfien 41170 pellexlem4 41184 pellexlem5 41185 ttac 41389 idomodle 41552 idomsubgmo 41554 iscard5 41882 uzct 43345 rn1st 43576 smfaddlem2 45079 smfmullem4 45109 smfpimbor1lem1 45113 aacllem 47322 |
Copyright terms: Public domain | W3C validator |