Metamath Proof Explorer

Theorem fliftfund

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016)

		Ref	Expression
	Hypotheses	flift.1	$⊢ F = ran (x \in X ⟼ ⟨A, B⟩)$
		flift.2	$⊢ (φ \land x \in X) \to A \in R$
		flift.3	$⊢ (φ \land x \in X) \to B \in S$
		fliftfun.4	$⊢ x = y \to A = C$
		fliftfun.5	$⊢ x = y \to B = D$
		fliftfund.6	$⊢ (φ \land (x \in X \land y \in X \land A = C)) \to B = D$
	Assertion	fliftfund	$⊢ φ \to Fun F$

Proof

Step	Hyp	Ref	Expression
1		flift.1	$⊢ F = ran (x \in X ⟼ ⟨A, B⟩)$
2		flift.2	$⊢ (φ \land x \in X) \to A \in R$
3		flift.3	$⊢ (φ \land x \in X) \to B \in S$
4		fliftfun.4	$⊢ x = y \to A = C$
5		fliftfun.5	$⊢ x = y \to B = D$
6		fliftfund.6	$⊢ (φ \land (x \in X \land y \in X \land A = C)) \to B = D$
7	6	3exp2	$⊢ φ \to (x \in X \to (y \in X \to (A = C \to B = D)))$
8	7	imp32	$⊢ (φ \land (x \in X \land y \in X)) \to (A = C \to B = D)$
9	8	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in X (A = C \to B = D)$
10	1 2 3 4 5	fliftfun	$⊢ φ \to (Fun F \leftrightarrow \forall x \in X \forall y \in X (A = C \to B = D))$
11	9 10	mpbird	$⊢ φ \to Fun F$