MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df1st2 Structured version   Visualization version   GIF version

Theorem df1st2 7784
Description: An alternate possible definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
df1st2 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝑥} = (1st ↾ (V × V))
Distinct variable group:   𝑥,𝑦,𝑧

Proof of Theorem df1st2
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 fo1st 7700 . . . . . 6 1st :V–onto→V
2 fofn 6589 . . . . . 6 (1st :V–onto→V → 1st Fn V)
31, 2ax-mp 5 . . . . 5 1st Fn V
4 dffn5 6721 . . . . 5 (1st Fn V ↔ 1st = (𝑤 ∈ V ↦ (1st𝑤)))
53, 4mpbi 231 . . . 4 1st = (𝑤 ∈ V ↦ (1st𝑤))
6 mptv 5168 . . . 4 (𝑤 ∈ V ↦ (1st𝑤)) = {⟨𝑤, 𝑧⟩ ∣ 𝑧 = (1st𝑤)}
75, 6eqtri 2849 . . 3 1st = {⟨𝑤, 𝑧⟩ ∣ 𝑧 = (1st𝑤)}
87reseq1i 5848 . 2 (1st ↾ (V × V)) = ({⟨𝑤, 𝑧⟩ ∣ 𝑧 = (1st𝑤)} ↾ (V × V))
9 resopab 5901 . 2 ({⟨𝑤, 𝑧⟩ ∣ 𝑧 = (1st𝑤)} ↾ (V × V)) = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (V × V) ∧ 𝑧 = (1st𝑤))}
10 vex 3503 . . . . 5 𝑥 ∈ V
11 vex 3503 . . . . 5 𝑦 ∈ V
1210, 11op1std 7690 . . . 4 (𝑤 = ⟨𝑥, 𝑦⟩ → (1st𝑤) = 𝑥)
1312eqeq2d 2837 . . 3 (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑧 = (1st𝑤) ↔ 𝑧 = 𝑥))
1413dfoprab3 7743 . 2 {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (V × V) ∧ 𝑧 = (1st𝑤))} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝑥}
158, 9, 143eqtrri 2854 1 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝑥} = (1st ↾ (V × V))
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1530  wcel 2107  Vcvv 3500  cop 4570  {copab 5125  cmpt 5143   × cxp 5552  cres 5556   Fn wfn 6347  ontowfo 6350  cfv 6352  {coprab 7149  1st c1st 7678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-fo 6358  df-fv 6360  df-oprab 7152  df-1st 7680  df-2nd 7681
This theorem is referenced by:  df1stres  30352
  Copyright terms: Public domain W3C validator