opfv

Description: Value of a function producing ordered pairs. (Contributed by Thierry Arnoux, 3-Jan-2017)

		Ref	Expression
	Assertion	opfv	$⊢ ((Fun F \land ran F \subseteq V \times V) \land x \in dom F) \to F (x) = ⟨(1^{st} \circ F) (x), (2^{nd} \circ F) (x)⟩$

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((Fun F \land ran F \subseteq V \times V) \land x \in dom F) \to ran F \subseteq V \times V$
2		fvelrn	$⊢ (Fun F \land x \in dom F) \to F (x) \in ran F$
3	2	adantlr	$⊢ ((Fun F \land ran F \subseteq V \times V) \land x \in dom F) \to F (x) \in ran F$
4	1 3	sseldd	$⊢ ((Fun F \land ran F \subseteq V \times V) \land x \in dom F) \to F (x) \in (V \times V)$
5		1st2ndb	$⊢ F (x) \in (V \times V) \leftrightarrow F (x) = ⟨1^{st} (F (x)), 2^{nd} (F (x))⟩$
6	4 5	sylib	$⊢ ((Fun F \land ran F \subseteq V \times V) \land x \in dom F) \to F (x) = ⟨1^{st} (F (x)), 2^{nd} (F (x))⟩$
7		fvco	$⊢ (Fun F \land x \in dom F) \to (1^{st} \circ F) (x) = 1^{st} (F (x))$
8		fvco	$⊢ (Fun F \land x \in dom F) \to (2^{nd} \circ F) (x) = 2^{nd} (F (x))$
9	7 8	opeq12d	$⊢ (Fun F \land x \in dom F) \to ⟨(1^{st} \circ F) (x), (2^{nd} \circ F) (x)⟩ = ⟨1^{st} (F (x)), 2^{nd} (F (x))⟩$
10	9	adantlr	$⊢ ((Fun F \land ran F \subseteq V \times V) \land x \in dom F) \to ⟨(1^{st} \circ F) (x), (2^{nd} \circ F) (x)⟩ = ⟨1^{st} (F (x)), 2^{nd} (F (x))⟩$
11	6 10	eqtr4d	$⊢ ((Fun F \land ran F \subseteq V \times V) \land x \in dom F) \to F (x) = ⟨(1^{st} \circ F) (x), (2^{nd} \circ F) (x)⟩$

Metamath Proof Explorer