qliftf

Description: The domain and codomain of the function F . (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$
Assertion	qliftf	$⊢ φ \to (Fun F \leftrightarrow F : X / R ⟶ Y)$

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	1 2 3 4	qliftlem	$⊢ (φ \land x \in X) \to [x] R \in (X / R)$
6	1 5 2	fliftf	$⊢ φ \to (Fun F \leftrightarrow F : ran (x \in X ⟼ [x] R) ⟶ Y)$
7		df-qs	$⊢ X / R = \{y \| \exists x \in X y = [x] R\}$
8		eqid	$⊢ (x \in X ⟼ [x] R) = (x \in X ⟼ [x] R)$
9	8	rnmpt	$⊢ ran (x \in X ⟼ [x] R) = \{y \| \exists x \in X y = [x] R\}$
10	7 9	eqtr4i	$⊢ X / R = ran (x \in X ⟼ [x] R)$
11	10	a1i	$⊢ φ \to X / R = ran (x \in X ⟼ [x] R)$
12	11	feq2d	$⊢ φ \to (F : X / R ⟶ Y \leftrightarrow F : ran (x \in X ⟼ [x] R) ⟶ Y)$
13	6 12	bitr4d	$⊢ φ \to (Fun F \leftrightarrow F : X / R ⟶ Y)$

Metamath Proof Explorer