Theorem 1st2val

Description: Value of an alternate definition of the 1st function. (Contributed by NM, 14-Oct-2004) (Revised by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Assertion	1st2val	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=1^{st}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		elvv	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists w\exists vA=⟨w,v⟩$$
2		fveq2	$$⊢A=⟨w,v⟩\to \left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=\left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(⟨w,v⟩\right)$$
3		df-ov	$$⊢w\left\{⟨⟨x,y⟩,z⟩|z=x\right\}v=\left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(⟨w,v⟩\right)$$
4		simpl	$$⊢\left(x=w\wedge y=v\right)\to x=w$$
5		mpov	$$⊢\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\right)=\left\{⟨⟨x,y⟩,z⟩|z=x\right\}$$
6	5	eqcomi	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=x\right\}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼x\right)$$
7		vex	$$⊢w\in \mathrm{V}$$
8	4 6 7	ovmpoa	$$⊢\left(w\in \mathrm{V}\wedge v\in \mathrm{V}\right)\to w\left\{⟨⟨x,y⟩,z⟩|z=x\right\}v=w$$
9	8	el2v	$$⊢w\left\{⟨⟨x,y⟩,z⟩|z=x\right\}v=w$$
10	3 9	eqtr3i	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(⟨w,v⟩\right)=w$$
11	2 10	eqtrdi	$$⊢A=⟨w,v⟩\to \left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=w$$
12		vex	$$⊢v\in \mathrm{V}$$
13	7 12	op1std	$$⊢A=⟨w,v⟩\to 1^{st}\left(A\right)=w$$
14	11 13	eqtr4d	$$⊢A=⟨w,v⟩\to \left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=1^{st}\left(A\right)$$
15	14	exlimivv	$$⊢\exists w\exists vA=⟨w,v⟩\to \left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=1^{st}\left(A\right)$$
16	1 15	sylbi	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=1^{st}\left(A\right)$$
17		vex	$$⊢x\in \mathrm{V}$$
18		vex	$$⊢y\in \mathrm{V}$$
19	17 18	pm3.2i	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)$$
20		ax6ev	$$⊢\exists zz=x$$
21	19 20	2th	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\leftrightarrow \exists zz=x$$
22	21	opabbii	$$⊢\left\{⟨x,y⟩|\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\right\}=\left\{⟨x,y⟩|\exists zz=x\right\}$$
23		df-xp	$$⊢\mathrm{V}\times \mathrm{V}=\left\{⟨x,y⟩|\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\right\}$$
24		dmoprab	$$⊢\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|z=x\right\}=\left\{⟨x,y⟩|\exists zz=x\right\}$$
25	22 23 24	3eqtr4ri	$$⊢\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|z=x\right\}=\mathrm{V}\times \mathrm{V}$$
26	25	eleq2i	$$⊢A\in \mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|z=x\right\}\leftrightarrow A\in \left(\mathrm{V}\times \mathrm{V}\right)$$
27		ndmfv	$$⊢\neg A\in \mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|z=x\right\}\to \left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=\varnothing$$
28	26 27	sylnbir	$$⊢\neg A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=\varnothing$$
29		dmsnn0	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \mathrm{dom}\left\{A\right\}\ne \varnothing$$
30	29	biimpri	$$⊢\mathrm{dom}\left\{A\right\}\ne \varnothing \to A\in \left(\mathrm{V}\times \mathrm{V}\right)$$
31	30	necon1bi	$$⊢\neg A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{dom}\left\{A\right\}=\varnothing$$
32	31	unieqd	$$⊢\neg A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \bigcup \mathrm{dom}\left\{A\right\}=\bigcup \varnothing$$
33		uni0	$$⊢\bigcup \varnothing =\varnothing$$
34	32 33	eqtrdi	$$⊢\neg A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \bigcup \mathrm{dom}\left\{A\right\}=\varnothing$$
35	28 34	eqtr4d	$$⊢\neg A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=\bigcup \mathrm{dom}\left\{A\right\}$$
36		1stval	$$⊢1^{st}\left(A\right)=\bigcup \mathrm{dom}\left\{A\right\}$$
37	35 36	eqtr4di	$$⊢\neg A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=1^{st}\left(A\right)$$
38	16 37	pm2.61i	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=x\right\}\left(A\right)=1^{st}\left(A\right)$$