This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qliftfund

Description: The function F is the unique function defined by F[ x ] = A , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

		Ref	Expression
	Hypotheses	qlift.1	$⊢ F = ran (x \in X ⟼ ⟨[x] R, A⟩)$
		qlift.2	$⊢ (φ \land x \in X) \to A \in Y$
		qlift.3	$⊢ φ \to R Er X$
		qlift.4	$⊢ φ \to X \in V$
		qliftfun.4	$⊢ x = y \to A = B$
		qliftfund.6	$⊢ (φ \land x R y) \to A = B$
	Assertion	qliftfund	$⊢ φ \to Fun F$

Proof

Step	Hyp	Ref	Expression
1		qlift.1	$⊢ F = ran (x \in X ⟼ ⟨[x] R, A⟩)$
2		qlift.2	$⊢ (φ \land x \in X) \to A \in Y$
3		qlift.3	$⊢ φ \to R Er X$
4		qlift.4	$⊢ φ \to X \in V$
5		qliftfun.4	$⊢ x = y \to A = B$
6		qliftfund.6	$⊢ (φ \land x R y) \to A = B$
7	6	ex	$⊢ φ \to (x R y \to A = B)$
8	7	alrimivv	$⊢ φ \to \forall x \forall y (x R y \to A = B)$
9	1 2 3 4 5	qliftfun	$⊢ φ \to (Fun F \leftrightarrow \forall x \forall y (x R y \to A = B))$
10	8 9	mpbird	$⊢ φ \to Fun F$