Metamath Proof Explorer

Theorem f1ofveu

Description: There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006)

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

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} : B \underset{1-1 onto}{⟶} A$
2		f1of	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} A \to F^{-1} : B ⟶ A$
3	1 2	syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} : B ⟶ A$
4		feu	$⊢ (F^{-1} : B ⟶ A \land C \in B) \to \exists! x \in A ⟨C, x⟩ \in F^{-1}$
5	3 4	sylan	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B) \to \exists! x \in A ⟨C, x⟩ \in F^{-1}$
6		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)$
7	6	3com23	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B \land x \in A) \to (F (x) = C \leftrightarrow F^{-1} (C) = x)$
8		dff1o4	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F Fn A \land F^{-1} Fn B)$
9	8	simprbi	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} Fn B$
10		fnopfvb	$⊢ (F^{-1} Fn B \land C \in B) \to (F^{-1} (C) = x \leftrightarrow ⟨C, x⟩ \in F^{-1})$
11	10	3adant3	$⊢ (F^{-1} Fn B \land C \in B \land x \in A) \to (F^{-1} (C) = x \leftrightarrow ⟨C, x⟩ \in F^{-1})$
12	9 11	syl3an1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B \land x \in A) \to (F^{-1} (C) = x \leftrightarrow ⟨C, x⟩ \in F^{-1})$
13	7 12	bitrd	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B \land x \in A) \to (F (x) = C \leftrightarrow ⟨C, x⟩ \in F^{-1})$
14	13	3expa	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land C \in B) \land x \in A) \to (F (x) = C \leftrightarrow ⟨C, x⟩ \in F^{-1})$
15	14	reubidva	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B) \to (\exists! x \in A F (x) = C \leftrightarrow \exists! x \in A ⟨C, x⟩ \in F^{-1})$
16	5 15	mpbird	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B) \to \exists! x \in A F (x) = C$