Metamath Proof Explorer

Theorem f1ocnvfv3

Description: Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006) (Proof shortened by Mario Carneiro, 24-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		f1ocnvdm	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B) \to F^{-1} (C) \in A$
2		f1ocnvfvb	$⊢ (F : A \underset{1-1 onto}{⟶} B \land x \in A \land C \in B) \to (F (x) = C \leftrightarrow F^{-1} (C) = x)$
3	2	3expa	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land x \in A) \land C \in B) \to (F (x) = C \leftrightarrow F^{-1} (C) = x)$
4	3	an32s	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land C \in B) \land x \in A) \to (F (x) = C \leftrightarrow F^{-1} (C) = x)$
5		eqcom	$⊢ x = F^{-1} (C) \leftrightarrow F^{-1} (C) = x$
6	4 5	bitr4di	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land C \in B) \land x \in A) \to (F (x) = C \leftrightarrow x = F^{-1} (C))$
7	1 6	riota5	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B) \to (ι x \in A \| F (x) = C) = F^{-1} (C)$
8	7	eqcomd	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B) \to F^{-1} (C) = (ι x \in A \| F (x) = C)$