f1ocnvfv1

Description: The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004)

		Ref	Expression
	Assertion	f1ocnvfv1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in A) \to F^{-1} (F (C)) = C$

Step	Hyp	Ref	Expression
1		f1ococnv1	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} \circ F = {I ↾}_{A}$
2	1	fveq1d	$⊢ F : A \underset{1-1 onto}{⟶} B \to (F^{-1} \circ F) (C) = ({I ↾}_{A}) (C)$
3	2	adantr	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in A) \to (F^{-1} \circ F) (C) = ({I ↾}_{A}) (C)$
4		f1of	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A ⟶ B$
5		fvco3	$⊢ (F : A ⟶ B \land C \in A) \to (F^{-1} \circ F) (C) = F^{-1} (F (C))$
6	4 5	sylan	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in A) \to (F^{-1} \circ F) (C) = F^{-1} (F (C))$
7		fvresi	$⊢ C \in A \to ({I ↾}_{A}) (C) = C$
8	7	adantl	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in A) \to ({I ↾}_{A}) (C) = C$
9	3 6 8	3eqtr3d	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in A) \to F^{-1} (F (C)) = C$

Metamath Proof Explorer