f1ocnvfv2

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

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

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

Metamath Proof Explorer