qliftfun

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$
Assertion	qliftfun	$⊢ φ \to (Fun F \leftrightarrow \forall x \forall y (x R y \to A = B))$

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	1 2 3 4	qliftlem	$⊢ (φ \land x \in X) \to [x] R \in (X / R)$
7		eceq1	$⊢ x = y \to [x] R = [y] R$
8	1 6 2 7 5	fliftfun	$⊢ φ \to (Fun F \leftrightarrow \forall x \in X \forall y \in X ([x] R = [y] R \to A = B))$
9	3	adantr	$⊢ (φ \land x R y) \to R Er X$
10		simpr	$⊢ (φ \land x R y) \to x R y$
11	9 10	ercl	$⊢ (φ \land x R y) \to x \in X$
12	9 10	ercl2	$⊢ (φ \land x R y) \to y \in X$
13	11 12	jca	$⊢ (φ \land x R y) \to (x \in X \land y \in X)$
14	13	ex	$⊢ φ \to (x R y \to (x \in X \land y \in X))$
15	14	pm4.71rd	$⊢ φ \to (x R y \leftrightarrow ((x \in X \land y \in X) \land x R y))$
16	3	adantr	$⊢ (φ \land (x \in X \land y \in X)) \to R Er X$
17		simprl	$⊢ (φ \land (x \in X \land y \in X)) \to x \in X$
18	16 17	erth	$⊢ (φ \land (x \in X \land y \in X)) \to (x R y \leftrightarrow [x] R = [y] R)$
19	18	pm5.32da	$⊢ φ \to (((x \in X \land y \in X) \land x R y) \leftrightarrow ((x \in X \land y \in X) \land [x] R = [y] R))$
20	15 19	bitrd	$⊢ φ \to (x R y \leftrightarrow ((x \in X \land y \in X) \land [x] R = [y] R))$
21	20	imbi1d	$⊢ φ \to ((x R y \to A = B) \leftrightarrow (((x \in X \land y \in X) \land [x] R = [y] R) \to A = B))$
22		impexp	$⊢ (((x \in X \land y \in X) \land [x] R = [y] R) \to A = B) \leftrightarrow ((x \in X \land y \in X) \to ([x] R = [y] R \to A = B))$
23	21 22	bitrdi	$⊢ φ \to ((x R y \to A = B) \leftrightarrow ((x \in X \land y \in X) \to ([x] R = [y] R \to A = B)))$
24	23	2albidv	$⊢ φ \to (\forall x \forall y (x R y \to A = B) \leftrightarrow \forall x \forall y ((x \in X \land y \in X) \to ([x] R = [y] R \to A = B)))$
25		r2al	$⊢ \forall x \in X \forall y \in X ([x] R = [y] R \to A = B) \leftrightarrow \forall x \forall y ((x \in X \land y \in X) \to ([x] R = [y] R \to A = B))$
26	24 25	bitr4di	$⊢ φ \to (\forall x \forall y (x R y \to A = B) \leftrightarrow \forall x \in X \forall y \in X ([x] R = [y] R \to A = B))$
27	8 26	bitr4d	$⊢ φ \to (Fun F \leftrightarrow \forall x \forall y (x R y \to A = B))$

Metamath Proof Explorer

Theorem qliftfun

Proof