Theorem 2nd2val

Description: Value of an alternate definition of the 2nd function. (Contributed by NM, 10-Aug-2006) (Revised by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Assertion	2nd2val	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(A\right)=2^{nd}\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=y\right\}\left(A\right)=\left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(⟨w,v⟩\right)$$
3		df-ov	$$⊢w\left\{⟨⟨x,y⟩,z⟩|z=y\right\}v=\left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(⟨w,v⟩\right)$$
4		simpr	$$⊢\left(x=w\wedge y=v\right)\to y=v$$
5		mpov	$$⊢\left(x\in \mathrm{V},y\in \mathrm{V}⟼y\right)=\left\{⟨⟨x,y⟩,z⟩|z=y\right\}$$
6	5	eqcomi	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=y\right\}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼y\right)$$
7		vex	$$⊢v\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=y\right\}v=v$$
9	8	el2v	$$⊢w\left\{⟨⟨x,y⟩,z⟩|z=y\right\}v=v$$
10	3 9	eqtr3i	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(⟨w,v⟩\right)=v$$
11	2 10	eqtrdi	$$⊢A=⟨w,v⟩\to \left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(A\right)=v$$
12		vex	$$⊢w\in \mathrm{V}$$
13	12 7	op2ndd	$$⊢A=⟨w,v⟩\to 2^{nd}\left(A\right)=v$$
14	11 13	eqtr4d	$$⊢A=⟨w,v⟩\to \left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(A\right)=2^{nd}\left(A\right)$$
15	14	exlimivv	$$⊢\exists w\exists vA=⟨w,v⟩\to \left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(A\right)=2^{nd}\left(A\right)$$
16	1 15	sylbi	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(A\right)=2^{nd}\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=y$$
21	19 20	2th	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\leftrightarrow \exists zz=y$$
22	21	opabbii	$$⊢\left\{⟨x,y⟩|\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\right\}=\left\{⟨x,y⟩|\exists zz=y\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=y\right\}=\left\{⟨x,y⟩|\exists zz=y\right\}$$
25	22 23 24	3eqtr4ri	$$⊢\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|z=y\right\}=\mathrm{V}\times \mathrm{V}$$
26	25	eleq2i	$$⊢A\in \mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|z=y\right\}\leftrightarrow A\in \left(\mathrm{V}\times \mathrm{V}\right)$$
27		ndmfv	$$⊢\neg A\in \mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|z=y\right\}\to \left\{⟨⟨x,y⟩,z⟩|z=y\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=y\right\}\left(A\right)=\varnothing$$
29		rnsnn0	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \mathrm{ran}\left\{A\right\}\ne \varnothing$$
30	29	biimpri	$$⊢\mathrm{ran}\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{ran}\left\{A\right\}=\varnothing$$
32	31	unieqd	$$⊢\neg A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \bigcup \mathrm{ran}\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{ran}\left\{A\right\}=\varnothing$$
35	28 34	eqtr4d	$$⊢\neg A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(A\right)=\bigcup \mathrm{ran}\left\{A\right\}$$
36		2ndval	$$⊢2^{nd}\left(A\right)=\bigcup \mathrm{ran}\left\{A\right\}$$
37	35 36	eqtr4di	$$⊢\neg A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(A\right)=2^{nd}\left(A\right)$$
38	16 37	pm2.61i	$$⊢\left\{⟨⟨x,y⟩,z⟩|z=y\right\}\left(A\right)=2^{nd}\left(A\right)$$