![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fo2nd | Structured version Visualization version GIF version |
Description: The 2nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Ref | Expression |
---|---|
fo2nd | ⊢ 2nd :V–onto→V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vsnex 5437 | . . . . 5 ⊢ {𝑥} ∈ V | |
2 | 1 | rnex 7925 | . . . 4 ⊢ ran {𝑥} ∈ V |
3 | 2 | uniex 7754 | . . 3 ⊢ ∪ ran {𝑥} ∈ V |
4 | df-2nd 8006 | . . 3 ⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) | |
5 | 3, 4 | fnmpti 6706 | . 2 ⊢ 2nd Fn V |
6 | 4 | rnmpt 5963 | . . 3 ⊢ ran 2nd = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}} |
7 | vex 3466 | . . . . 5 ⊢ 𝑦 ∈ V | |
8 | opex 5472 | . . . . . 6 ⊢ 〈𝑦, 𝑦〉 ∈ V | |
9 | 7, 7 | op2nda 6241 | . . . . . . 7 ⊢ ∪ ran {〈𝑦, 𝑦〉} = 𝑦 |
10 | 9 | eqcomi 2735 | . . . . . 6 ⊢ 𝑦 = ∪ ran {〈𝑦, 𝑦〉} |
11 | sneq 4643 | . . . . . . . . 9 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → {𝑥} = {〈𝑦, 𝑦〉}) | |
12 | 11 | rneqd 5946 | . . . . . . . 8 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → ran {𝑥} = ran {〈𝑦, 𝑦〉}) |
13 | 12 | unieqd 4928 | . . . . . . 7 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → ∪ ran {𝑥} = ∪ ran {〈𝑦, 𝑦〉}) |
14 | 13 | rspceeqv 3630 | . . . . . 6 ⊢ ((〈𝑦, 𝑦〉 ∈ V ∧ 𝑦 = ∪ ran {〈𝑦, 𝑦〉}) → ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}) |
15 | 8, 10, 14 | mp2an 690 | . . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥} |
16 | 7, 15 | 2th 263 | . . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}) |
17 | 16 | eqabi 2862 | . . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}} |
18 | 6, 17 | eqtr4i 2757 | . 2 ⊢ ran 2nd = V |
19 | df-fo 6562 | . 2 ⊢ (2nd :V–onto→V ↔ (2nd Fn V ∧ ran 2nd = V)) | |
20 | 5, 18, 19 | mpbir2an 709 | 1 ⊢ 2nd :V–onto→V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∈ wcel 2099 {cab 2703 ∃wrex 3060 Vcvv 3462 {csn 4633 〈cop 4639 ∪ cuni 4915 ran crn 5685 Fn wfn 6551 –onto→wfo 6554 2nd c2nd 8004 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5306 ax-nul 5313 ax-pr 5435 ax-un 7748 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4916 df-br 5156 df-opab 5218 df-mpt 5239 df-id 5582 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-fun 6558 df-fn 6559 df-fo 6562 df-2nd 8006 |
This theorem is referenced by: br2ndeqg 8028 2ndcof 8036 df2nd2 8115 2ndconst 8117 opco2 8140 iunfo 10584 cdaf 18074 2ndf1 18221 2ndf2 18222 2ndfcl 18224 gsum2dlem2 19971 upxp 23621 uptx 23623 cnmpt2nd 23667 uniiccdif 25601 precsexlem10 28218 precsexlem11 28219 xppreima 32565 2ndimaxp 32566 2ndresdju 32568 xppreima2 32570 2ndpreima 32621 fsuppcurry1 32641 gsummpt2d 32919 gsumpart 32925 cnre2csqima 33728 filnetlem4 36095 |
Copyright terms: Public domain | W3C validator |