Metamath Proof Explorer

Theorem 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 e. X |-> <. [ x ] R , A >. )
qlift.2 
|- ( ( ph /\ x e. X ) -> A e. Y )
qlift.3 
|- ( ph -> R Er X )
qlift.4 
|- ( ph -> X e. V )
qliftfun.4 
|- ( x = y -> A = B )
Assertion qliftfun 
|- ( ph -> ( Fun F <-> A. x A. y ( x R y -> A = B ) ) )

Proof

Step Hyp Ref Expression
1 qlift.1 
 |-  F = ran ( x e. X |-> <. [ x ] R , A >. )
2 qlift.2 
 |-  ( ( ph /\ x e. X ) -> A e. Y )
3 qlift.3 
 |-  ( ph -> R Er X )
4 qlift.4 
 |-  ( ph -> X e. V )
5 qliftfun.4 
 |-  ( x = y -> A = B )
6 1 2 3 4 qliftlem 
 |-  ( ( ph /\ x e. X ) -> [ x ] R e. ( X /. R ) )
7 eceq1 
 |-  ( x = y -> [ x ] R = [ y ] R )
8 1 6 2 7 5 fliftfun 
 |-  ( ph -> ( Fun F <-> A. x e. X A. y e. X ( [ x ] R = [ y ] R -> A = B ) ) )
9 3 adantr 
 |-  ( ( ph /\ x R y ) -> R Er X )
10 simpr 
 |-  ( ( ph /\ x R y ) -> x R y )
11 9 10 ercl 
 |-  ( ( ph /\ x R y ) -> x e. X )
12 9 10 ercl2 
 |-  ( ( ph /\ x R y ) -> y e. X )
13 11 12 jca 
 |-  ( ( ph /\ x R y ) -> ( x e. X /\ y e. X ) )
14 13 ex 
 |-  ( ph -> ( x R y -> ( x e. X /\ y e. X ) ) )
15 14 pm4.71rd 
 |-  ( ph -> ( x R y <-> ( ( x e. X /\ y e. X ) /\ x R y ) ) )
16 3 adantr 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> R Er X )
17 simprl 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> x e. X )
18 16 17 erth 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x R y <-> [ x ] R = [ y ] R ) )
19 18 pm5.32da 
 |-  ( ph -> ( ( ( x e. X /\ y e. X ) /\ x R y ) <-> ( ( x e. X /\ y e. X ) /\ [ x ] R = [ y ] R ) ) )
20 15 19 bitrd 
 |-  ( ph -> ( x R y <-> ( ( x e. X /\ y e. X ) /\ [ x ] R = [ y ] R ) ) )
21 20 imbi1d 
 |-  ( ph -> ( ( x R y -> A = B ) <-> ( ( ( x e. X /\ y e. X ) /\ [ x ] R = [ y ] R ) -> A = B ) ) )
22 impexp 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ [ x ] R = [ y ] R ) -> A = B ) <-> ( ( x e. X /\ y e. X ) -> ( [ x ] R = [ y ] R -> A = B ) ) )
23 21 22 bitrdi 
 |-  ( ph -> ( ( x R y -> A = B ) <-> ( ( x e. X /\ y e. X ) -> ( [ x ] R = [ y ] R -> A = B ) ) ) )
24 23 2albidv 
 |-  ( ph -> ( A. x A. y ( x R y -> A = B ) <-> A. x A. y ( ( x e. X /\ y e. X ) -> ( [ x ] R = [ y ] R -> A = B ) ) ) )
25 r2al 
 |-  ( A. x e. X A. y e. X ( [ x ] R = [ y ] R -> A = B ) <-> A. x A. y ( ( x e. X /\ y e. X ) -> ( [ x ] R = [ y ] R -> A = B ) ) )
26 24 25 bitr4di 
 |-  ( ph -> ( A. x A. y ( x R y -> A = B ) <-> A. x e. X A. y e. X ( [ x ] R = [ y ] R -> A = B ) ) )
27 8 26 bitr4d 
 |-  ( ph -> ( Fun F <-> A. x A. y ( x R y -> A = B ) ) )