![]() |
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 5036 | . . . . 5 ⊢ {𝑥} ∈ V | |
2 | 1 | dmex 7245 | . . . 4 ⊢ dom {𝑥} ∈ V |
3 | 2 | uniex 7099 | . . 3 ⊢ ∪ dom {𝑥} ∈ V |
4 | df-1st 7314 | . . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥}) | |
5 | 3, 4 | fnmpti 6162 | . 2 ⊢ 1st Fn V |
6 | 4 | rnmpt 5509 | . . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}} |
7 | vex 3352 | . . . . 5 ⊢ 𝑦 ∈ V | |
8 | opex 5060 | . . . . . 6 ⊢ 〈𝑦, 𝑦〉 ∈ V | |
9 | 7, 7 | op1sta 5760 | . . . . . . 7 ⊢ ∪ dom {〈𝑦, 𝑦〉} = 𝑦 |
10 | 9 | eqcomi 2779 | . . . . . 6 ⊢ 𝑦 = ∪ dom {〈𝑦, 𝑦〉} |
11 | sneq 4324 | . . . . . . . . . 10 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → {𝑥} = {〈𝑦, 𝑦〉}) | |
12 | 11 | dmeqd 5464 | . . . . . . . . 9 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → dom {𝑥} = dom {〈𝑦, 𝑦〉}) |
13 | 12 | unieqd 4582 | . . . . . . . 8 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → ∪ dom {𝑥} = ∪ dom {〈𝑦, 𝑦〉}) |
14 | 13 | eqeq2d 2780 | . . . . . . 7 ⊢ (𝑥 = 〈𝑦, 𝑦〉 → (𝑦 = ∪ dom {𝑥} ↔ 𝑦 = ∪ dom {〈𝑦, 𝑦〉})) |
15 | 14 | rspcev 3458 | . . . . . 6 ⊢ ((〈𝑦, 𝑦〉 ∈ V ∧ 𝑦 = ∪ dom {〈𝑦, 𝑦〉}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}) |
16 | 8, 10, 15 | mp2an 664 | . . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥} |
17 | 7, 16 | 2th 254 | . . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}) |
18 | 17 | abbi2i 2886 | . . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}} |
19 | 6, 18 | eqtr4i 2795 | . 2 ⊢ ran 1st = V |
20 | df-fo 6037 | . 2 ⊢ (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V)) | |
21 | 5, 19, 20 | mpbir2an 682 | 1 ⊢ 1st :V–onto→V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1630 ∈ wcel 2144 {cab 2756 ∃wrex 3061 Vcvv 3349 {csn 4314 〈cop 4320 ∪ cuni 4572 dom cdm 5249 ran crn 5250 Fn wfn 6026 –onto→wfo 6029 1st c1st 7312 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-8 2146 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 ax-sep 4912 ax-nul 4920 ax-pr 5034 ax-un 7095 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3an 1072 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-eu 2621 df-mo 2622 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ral 3065 df-rex 3066 df-rab 3069 df-v 3351 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-nul 4062 df-if 4224 df-sn 4315 df-pr 4317 df-op 4321 df-uni 4573 df-br 4785 df-opab 4845 df-mpt 4862 df-id 5157 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-fun 6033 df-fn 6034 df-fo 6037 df-1st 7314 |
This theorem is referenced by: br1steqg 7336 1stcof 7344 df1st2 7413 1stconst 7415 fsplit 7432 algrflem 7436 fpwwe 9669 axpre-sup 10191 homadm 16896 homacd 16897 dmaf 16905 cdaf 16906 1stf1 17039 1stf2 17040 1stfcl 17044 upxp 21646 uptx 21648 cnmpt1st 21691 bcthlem4 23342 uniiccdif 23565 vafval 27792 smfval 27794 0vfval 27795 vsfval 27822 xppreima 29783 xppreima2 29784 1stpreimas 29817 1stpreima 29818 gsummpt2d 30115 cnre2csqima 30291 poimirlem26 33761 poimirlem27 33762 |
Copyright terms: Public domain | W3C validator |