f1mptrn

Description: Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020)

Step	Hyp	Ref	Expression
1		f1mptrn.1	$⊢ (φ \land x \in A) \to B \in C$
2		f1mptrn.2	$⊢ (φ \land y \in C) \to \exists! x \in A y = B$
3	1	ralrimiva	$⊢ φ \to \forall x \in A B \in C$
4	2	ralrimiva	$⊢ φ \to \forall y \in C \exists! x \in A y = B$
5		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
6	5	f1ompt	$⊢ (x \in A ⟼ B) : A \underset{1-1 onto}{⟶} C \leftrightarrow (\forall x \in A B \in C \land \forall y \in C \exists! x \in A y = B)$
7		dff1o2	$⊢ (x \in A ⟼ B) : A \underset{1-1 onto}{⟶} C \leftrightarrow ((x \in A ⟼ B) Fn A \land Fun {(x \in A ⟼ B)}^{-1} \land ran (x \in A ⟼ B) = C)$
8	7	simp2bi	$⊢ (x \in A ⟼ B) : A \underset{1-1 onto}{⟶} C \to Fun {(x \in A ⟼ B)}^{-1}$
9	6 8	sylbir	$⊢ (\forall x \in A B \in C \land \forall y \in C \exists! x \in A y = B) \to Fun {(x \in A ⟼ B)}^{-1}$
10	3 4 9	syl2anc	$⊢ φ \to Fun {(x \in A ⟼ B)}^{-1}$

Metamath Proof Explorer