Metamath Proof Explorer


Theorem qliftf

Description: The domain and range 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 X x R A
qlift.2 φ x X A Y
qlift.3 φ R Er X
qlift.4 φ X V
Assertion qliftf φ Fun F F : X / R Y

Proof

Step Hyp Ref Expression
1 qlift.1 F = ran x X x R A
2 qlift.2 φ x X A Y
3 qlift.3 φ R Er X
4 qlift.4 φ X V
5 1 2 3 4 qliftlem φ x X x R X / R
6 1 5 2 fliftf φ Fun F F : ran x X x R Y
7 df-qs X / R = y | x X y = x R
8 eqid x X x R = x X x R
9 8 rnmpt ran x X x R = y | x X y = x R
10 7 9 eqtr4i X / R = ran x X x R
11 10 a1i φ X / R = ran x X x R
12 11 feq2d φ F : X / R Y F : ran x X x R Y
13 6 12 bitr4d φ Fun F F : X / R Y