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 5355 | . . . . 5 ⊢ {𝑥} ∈ V | |
2 | 1 | rnex 7768 | . . . 4 ⊢ ran {𝑥} ∈ V |
3 | 2 | uniex 7603 | . . 3 ⊢ ∪ ran {𝑥} ∈ V |
4 | df-2nd 7841 | . . 3 ⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥}) | |
5 | 3, 4 | fnmpti 6585 | . 2 ⊢ 2nd Fn V |
6 | 4 | rnmpt 5867 | . . 3 ⊢ ran 2nd = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}} |
7 | vex 3437 | . . . . 5 ⊢ 𝑦 ∈ V | |
8 | opex 5380 | . . . . . 6 ⊢ 〈𝑦, 𝑦〉 ∈ V | |
9 | 7, 7 | op2nda 6136 | . . . . . . 7 ⊢ ∪ ran {〈𝑦, 𝑦〉} = 𝑦 |
10 | 9 | eqcomi 2748 | . . . . . 6 ⊢ 𝑦 = ∪ ran {〈𝑦, 𝑦〉} |
11 | sneq 4572 | . . . . . . . . 9 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → {𝑥} = {〈𝑦, 𝑦〉}) | |
12 | 11 | rneqd 5850 | . . . . . . . 8 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → ran {𝑥} = ran {〈𝑦, 𝑦〉}) |
13 | 12 | unieqd 4854 | . . . . . . 7 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → ∪ ran {𝑥} = ∪ ran {〈𝑦, 𝑦〉}) |
14 | 13 | rspceeqv 3576 | . . . . . 6 ⊢ ((〈𝑦, 𝑦〉 ∈ V ∧ 𝑦 = ∪ ran {〈𝑦, 𝑦〉}) → ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}) |
15 | 8, 10, 14 | mp2an 689 | . . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥} |
16 | 7, 15 | 2th 263 | . . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}) |
17 | 16 | abbi2i 2880 | . . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}} |
18 | 6, 17 | eqtr4i 2770 | . 2 ⊢ ran 2nd = V |
19 | df-fo 6443 | . 2 ⊢ (2nd :V–onto→V ↔ (2nd Fn V ∧ ran 2nd = V)) | |
20 | 5, 18, 19 | mpbir2an 708 | 1 ⊢ 2nd :V–onto→V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∈ wcel 2107 {cab 2716 ∃wrex 3066 Vcvv 3433 {csn 4562 〈cop 4568 ∪ cuni 4840 ran crn 5591 Fn wfn 6432 –onto→wfo 6435 2nd c2nd 7839 |
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-11 2155 ax-12 2172 ax-ext 2710 ax-sep 5224 ax-nul 5231 ax-pr 5353 ax-un 7597 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3435 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4258 df-if 4461 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-br 5076 df-opab 5138 df-mpt 5159 df-id 5490 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-fun 6439 df-fn 6440 df-fo 6443 df-2nd 7841 |
This theorem is referenced by: br2ndeqg 7863 2ndcof 7871 df2nd2 7948 2ndconst 7950 opco2 7974 iunfo 10304 cdaf 17774 2ndf1 17921 2ndf2 17922 2ndfcl 17924 gsum2dlem2 19581 upxp 22783 uptx 22785 cnmpt2nd 22829 uniiccdif 24751 xppreima 30992 2ndimaxp 30993 2ndresdju 30995 xppreima2 30997 2ndpreima 31049 fsuppcurry1 31069 gsummpt2d 31318 gsumpart 31324 cnre2csqima 31870 filnetlem4 34579 |
Copyright terms: Public domain | W3C validator |