Metamath Proof Explorer

Theorem opfv

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

		Ref	Expression
	Assertion	opfv	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		simplr	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ran 𝐹 ⊆ ( V × V ) )
2		fvelrn	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
3	2	adantlr	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
4	1 3	sseldd	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( V × V ) )
5		1st2ndb	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( V × V ) ↔ ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
6	4 5	sylib	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
7		fvco	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) = ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) )
8		fvco	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) )
9	7 8	opeq12d	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
10	9	adantlr	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
11	6 10	eqtr4d	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ )