Theorem 2ndval2

Description: Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of Monk1 p. 52. (Contributed by NM, 18-Aug-2006)

	Ref	Expression
Assertion	2ndval2	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to 2^{nd}\left(A\right)=\bigcap \bigcap \bigcap {\left\{A\right\}}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		elvv	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yA=⟨x,y⟩$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	op2nd	$$⊢2^{nd}\left(⟨x,y⟩\right)=y$$
5	2 3	op2ndb	$$⊢\bigcap \bigcap \bigcap {\left\{⟨x,y⟩\right\}}^{-1}=y$$
6	4 5	eqtr4i	$$⊢2^{nd}\left(⟨x,y⟩\right)=\bigcap \bigcap \bigcap {\left\{⟨x,y⟩\right\}}^{-1}$$
7		fveq2	$$⊢A=⟨x,y⟩\to 2^{nd}\left(A\right)=2^{nd}\left(⟨x,y⟩\right)$$
8		sneq	$$⊢A=⟨x,y⟩\to \left\{A\right\}=\left\{⟨x,y⟩\right\}$$
9	8	cnveqd	$$⊢A=⟨x,y⟩\to {\left\{A\right\}}^{-1}={\left\{⟨x,y⟩\right\}}^{-1}$$
10	9	inteqd	$$⊢A=⟨x,y⟩\to \bigcap {\left\{A\right\}}^{-1}=\bigcap {\left\{⟨x,y⟩\right\}}^{-1}$$
11	10	inteqd	$$⊢A=⟨x,y⟩\to \bigcap \bigcap {\left\{A\right\}}^{-1}=\bigcap \bigcap {\left\{⟨x,y⟩\right\}}^{-1}$$
12	11	inteqd	$$⊢A=⟨x,y⟩\to \bigcap \bigcap \bigcap {\left\{A\right\}}^{-1}=\bigcap \bigcap \bigcap {\left\{⟨x,y⟩\right\}}^{-1}$$
13	6 7 12	3eqtr4a	$$⊢A=⟨x,y⟩\to 2^{nd}\left(A\right)=\bigcap \bigcap \bigcap {\left\{A\right\}}^{-1}$$
14	13	exlimivv	$$⊢\exists x\exists yA=⟨x,y⟩\to 2^{nd}\left(A\right)=\bigcap \bigcap \bigcap {\left\{A\right\}}^{-1}$$
15	1 14	sylbi	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to 2^{nd}\left(A\right)=\bigcap \bigcap \bigcap {\left\{A\right\}}^{-1}$$