![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fo1st | Structured version Visualization version GIF version |
Description: The 1st function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Ref | Expression |
---|---|
fo1st | ⊢ 1st :V–onto→V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snex 5223 | . . . . 5 ⊢ {𝑥} ∈ V | |
2 | 1 | dmex 7472 | . . . 4 ⊢ dom {𝑥} ∈ V |
3 | 2 | uniex 7323 | . . 3 ⊢ ∪ dom {𝑥} ∈ V |
4 | df-1st 7545 | . . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) | |
5 | 3, 4 | fnmpti 6359 | . 2 ⊢ 1st Fn V |
6 | 4 | rnmpt 5709 | . . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}} |
7 | vex 3440 | . . . . 5 ⊢ 𝑦 ∈ V | |
8 | opex 5248 | . . . . . 6 ⊢ 〈𝑦, 𝑦〉 ∈ V | |
9 | 7, 7 | op1sta 5957 | . . . . . . 7 ⊢ ∪ dom {〈𝑦, 𝑦〉} = 𝑦 |
10 | 9 | eqcomi 2804 | . . . . . 6 ⊢ 𝑦 = ∪ dom {〈𝑦, 𝑦〉} |
11 | sneq 4482 | . . . . . . . . 9 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → {𝑥} = {〈𝑦, 𝑦〉}) | |
12 | 11 | dmeqd 5660 | . . . . . . . 8 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → dom {𝑥} = dom {〈𝑦, 𝑦〉}) |
13 | 12 | unieqd 4755 | . . . . . . 7 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → ∪ dom {𝑥} = ∪ dom {〈𝑦, 𝑦〉}) |
14 | 13 | rspceeqv 3577 | . . . . . 6 ⊢ ((〈𝑦, 𝑦〉 ∈ V ∧ 𝑦 = ∪ dom {〈𝑦, 𝑦〉}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}) |
15 | 8, 10, 14 | mp2an 688 | . . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥} |
16 | 7, 15 | 2th 265 | . . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}) |
17 | 16 | abbi2i 2922 | . . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}} |
18 | 6, 17 | eqtr4i 2822 | . 2 ⊢ ran 1st = V |
19 | df-fo 6231 | . 2 ⊢ (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V)) | |
20 | 5, 18, 19 | mpbir2an 707 | 1 ⊢ 1st :V–onto→V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ∈ wcel 2081 {cab 2775 ∃wrex 3106 Vcvv 3437 {csn 4472 〈cop 4478 ∪ cuni 4745 dom cdm 5443 ran crn 5444 Fn wfn 6220 –onto→wfo 6223 1st c1st 7543 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pr 5221 ax-un 7319 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-fun 6227 df-fn 6228 df-fo 6231 df-1st 7545 |
This theorem is referenced by: br1steqg 7567 1stcof 7575 df1st2 7649 1stconst 7651 fsplit 7668 algrflem 7672 fpwwe 9914 axpre-sup 10437 homadm 17129 homacd 17130 dmaf 17138 cdaf 17139 1stf1 17271 1stf2 17272 1stfcl 17276 upxp 21915 uptx 21917 cnmpt1st 21960 bcthlem4 23613 uniiccdif 23862 vafval 28071 smfval 28073 0vfval 28074 vsfval 28101 xppreima 30084 xppreima2 30085 1stpreimas 30129 1stpreima 30130 fsuppcurry2 30150 gsummpt2d 30496 cnre2csqima 30771 poimirlem26 34468 poimirlem27 34469 |
Copyright terms: Public domain | W3C validator |