![]() |
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 | snex 5130 | . . . . 5 ⊢ {𝑥} ∈ V | |
2 | 1 | rnex 7363 | . . . 4 ⊢ ran {𝑥} ∈ V |
3 | 2 | uniex 7214 | . . 3 ⊢ ∪ ran {𝑥} ∈ V |
4 | df-2nd 7430 | . . 3 ⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) | |
5 | 3, 4 | fnmpti 6256 | . 2 ⊢ 2nd Fn V |
6 | 4 | rnmpt 5605 | . . 3 ⊢ ran 2nd = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}} |
7 | vex 3418 | . . . . 5 ⊢ 𝑦 ∈ V | |
8 | opex 5154 | . . . . . 6 ⊢ 〈𝑦, 𝑦〉 ∈ V | |
9 | 7, 7 | op2nda 5863 | . . . . . . 7 ⊢ ∪ ran {〈𝑦, 𝑦〉} = 𝑦 |
10 | 9 | eqcomi 2835 | . . . . . 6 ⊢ 𝑦 = ∪ ran {〈𝑦, 𝑦〉} |
11 | sneq 4408 | . . . . . . . . 9 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → {𝑥} = {〈𝑦, 𝑦〉}) | |
12 | 11 | rneqd 5586 | . . . . . . . 8 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → ran {𝑥} = ran {〈𝑦, 𝑦〉}) |
13 | 12 | unieqd 4669 | . . . . . . 7 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → ∪ ran {𝑥} = ∪ ran {〈𝑦, 𝑦〉}) |
14 | 13 | rspceeqv 3545 | . . . . . 6 ⊢ ((〈𝑦, 𝑦〉 ∈ V ∧ 𝑦 = ∪ ran {〈𝑦, 𝑦〉}) → ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}) |
15 | 8, 10, 14 | mp2an 685 | . . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥} |
16 | 7, 15 | 2th 256 | . . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}) |
17 | 16 | abbi2i 2944 | . . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}} |
18 | 6, 17 | eqtr4i 2853 | . 2 ⊢ ran 2nd = V |
19 | df-fo 6130 | . 2 ⊢ (2nd :V–onto→V ↔ (2nd Fn V ∧ ran 2nd = V)) | |
20 | 5, 18, 19 | mpbir2an 704 | 1 ⊢ 2nd :V–onto→V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ∈ wcel 2166 {cab 2812 ∃wrex 3119 Vcvv 3415 {csn 4398 〈cop 4404 ∪ cuni 4659 ran crn 5344 Fn wfn 6119 –onto→wfo 6122 2nd c2nd 7428 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pr 5128 ax-un 7210 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-opab 4937 df-mpt 4954 df-id 5251 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-fun 6126 df-fn 6127 df-fo 6130 df-2nd 7430 |
This theorem is referenced by: br2ndeqg 7452 2ndcof 7460 df2nd2 7529 2ndconst 7531 iunfo 9677 cdaf 17053 2ndf1 17189 2ndf2 17190 2ndfcl 17192 gsum2dlem2 18724 upxp 21798 uptx 21800 cnmpt2nd 21844 uniiccdif 23745 xppreima 29999 xppreima2 30000 2ndpreima 30034 gsummpt2d 30327 cnre2csqima 30503 filnetlem4 32915 |
Copyright terms: Public domain | W3C validator |