Theorem df1st2 4119

Description: An alternate possible definition of the 1st function.

Assertion

Ref	Expression
df1st2	|- {<.<.x, y>., z>. | z = x} = (1st |` (V X. V))

Distinct variable group:   x,y,z

Proof of Theorem df1st2

Step	Hyp	Ref	Expression
1		visset 1810	. . . 4 |- x e. V
2		visset 1810	. . . . . . 7 |- y e. V
3	1, 2	pm3.2i 285	. . . . . 6 |- (x e. V /\ y e. V)
4	3	biantrur 724	. . . . 5 |- (z = x <-> ((x e. V /\ y e. V) /\ z = x))
5	4	oprabbii 3992	. . . 4 |- {<.<.x, y>., z>. | z = x} = {<.<.x, y>., z>. | ((x e. V /\ y e. V) /\ z = x)}
6	1, 5	fnoprab2 4115	. . 3 |- {<.<.x, y>., z>. | z = x} Fn (V X. V)
7		fo1st 4084	. . . . . 6 |- 1st:V-onto->V
8		fof 3667	. . . . . 6 |- (1st:V-onto->V -> 1st:V-->V)
9	7, 8	ax-mp 7	. . . . 5 |- 1st:V-->V
10		ffn 3623	. . . . 5 |- (1st:V-->V -> 1st Fn V)
11	9, 10	ax-mp 7	. . . 4 |- 1st Fn V
12		ssv 2078	. . . 4 |- (V X. V) (_ V
13		fnssres 3596	. . . 4 |- ((1st Fn V /\ (V X. V) (_ V) -> (1st |` (V X. V)) Fn (V X. V))
14	11, 12, 13	mp2an 696	. . 3 |- (1st |` (V X. V)) Fn (V X. V)
15		eqfnfv 3792	. . 3 |- (({<.<.x, y>., z>. | z = x} Fn (V X. V) /\ (1st |` (V X. V)) Fn (V X. V)) -> ({<.<.x, y>., z>. | z = x} = (1st |` (V X. V)) <-> ((V X. V) = (V X. V) /\ A.u e. (V X. V)({<.<.x, y>., z>. | z = x}` u) = ((1st |` (V X. V))` u))))
16	6, 14, 15	mp2an 696	. 2 |- ({<.<.x, y>., z>. | z = x} = (1st |` (V X. V)) <-> ((V X. V) = (V X. V) /\ A.u e. (V X. V)({<.<.x, y>., z>. | z = x}` u) = ((1st |` (V X. V))` u)))
17		eqid 1474	. 2 |- (V X. V) = (V X. V)
18		1st2val 4088	. . . . . 6 |- ({<.<.x, y>., z>. | z = x}` <.w, v>.) = (1st` <.w, v>.)
19		visset 1810	. . . . . . . . 9 |- v e. V
20	19	opelxp 3210	. . . . . . . 8 |- (<.w, v>. e. (V X. V) <-> (w e. V /\ v e. V))
21		visset 1810	. . . . . . . 8 |- w e. V
22	20, 21, 19	mpbir2an 729	. . . . . . 7 |- <.w, v>. e. (V X. V)
23		fvres 3729	. . . . . . 7 |- (<.w, v>. e. (V X. V) -> ((1st |` (V X. V))` <.w, v>.) = (1st` <.w, v>.))
24	22, 23	ax-mp 7	. . . . . 6 |- ((1st |` (V X. V))` <.w, v>.) = (1st` <.w, v>.)
25	18, 24	eqtr4 1496	. . . . 5 |- ({<.<.x, y>., z>. | z = x}` <.w, v>.) = ((1st |` (V X. V))` <.w, v>.)
26	25	a1i 8	. . . 4 |- ((w e. V /\ v e. V) -> ({<.<.x, y>., z>. | z = x}` <.w, v>.) = ((1st |` (V X. V))` <.w, v>.))
27	26	rgen2a 1697	. . 3 |- A.w e. V A.v e. V ({<.<.x, y>., z>. | z = x}` <.w, v>.) = ((1st |` (V X. V))` <.w, v>.)
28		fveq2 3719	. . . . 5 |- (u = <.w, v>. -> ({<.<.x, y>., z>. | z = x}` u) = ({<.<.x, y>., z>. | z = x}` <.w, v>.))
29		fveq2 3719	. . . . 5 |- (u = <.w, v>. -> ((1st |` (V X. V))` u) = ((1st |` (V X. V))` <.w, v>.))
30	28, 29	eqeq12d 1487	. . . 4 |- (u = <.w, v>. -> (({<.<.x, y>., z>. | z = x}` u) = ((1st |` (V X. V))` u) <-> ({<.<.x, y>., z>. | z = x}` <.w, v>.) = ((1st |` (V X. V))` <.w, v>.)))
31	30	ralxp 3214	. . 3 |- (A.u e. (V X. V)({<.<.x, y>., z>. | z = x}` u) = ((1st |` (V X. V))` u) <-> A.w e. V A.v e. V ({<.<.x, y>., z>. | z = x}` <.w, v>.) = ((1st |` (V X. V))` <.w, v>.))
32	27, 31	mpbir 190	. 2 |- A.u e. (V X. V)({<.<.x, y>., z>. | z = x}` u) = ((1st |` (V X. V))` u)
33	16, 17, 32	mpbir2an 729	1 |- {<.<.x, y>., z>. | z = x} = (1st |` (V X. V))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 955   e. wcel 957  A.wral 1643  Vcvv 1808   (_ wss 2044  <.cop 2408   X. cxp 3164   |` cres 3168   Fn wfn 3173  -->wf 3174  -onto->wfo 3176  ` cfv 3178  {copab2 3959  1stc1st 4070

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2862

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-v 1809  df-sbc 1939  df-csb 1999  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410  df-op 2413  df-uni 2500  df-br 2616  df-opab 2663  df-id 2831  df-xp 3180  df-rel 3181  df-cnv 3182  df-co 3183  df-dm 3184  df-rn 3185  df-res 3186  df-ima 3187  df-fun 3188  df-fn 3189  df-f 3190  df-fo 3192  df-fv 3194  df-opr 3960  df-oprab 3961  df-1st 4072  df-2nd 4073

Copyright terms: Public domain