This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (V \times V) \to 2^{nd} (A) = ⋂ ⋂ ⋂ {\{A\}}^{-1}$

Proof

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