Metamath Proof Explorer

Theorem fliftfun

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses flift.1 
|- F = ran ( x e. X |-> <. A , B >. )
flift.2 
|- ( ( ph /\ x e. X ) -> A e. R )
flift.3 
|- ( ( ph /\ x e. X ) -> B e. S )
fliftfun.4 
|- ( x = y -> A = C )
fliftfun.5 
|- ( x = y -> B = D )
Assertion fliftfun 
|- ( ph -> ( Fun F <-> A. x e. X A. y e. X ( A = C -> B = D ) ) )

Proof

Step Hyp Ref Expression
1 flift.1 
 |-  F = ran ( x e. X |-> <. A , B >. )
2 flift.2 
 |-  ( ( ph /\ x e. X ) -> A e. R )
3 flift.3 
 |-  ( ( ph /\ x e. X ) -> B e. S )
4 fliftfun.4 
 |-  ( x = y -> A = C )
5 fliftfun.5 
 |-  ( x = y -> B = D )
6 nfv 
 |-  F/ x ph
7 nfmpt1 
 |-  F/_ x ( x e. X |-> <. A , B >. )
8 7 nfrn 
 |-  F/_ x ran ( x e. X |-> <. A , B >. )
9 1 8 nfcxfr 
 |-  F/_ x F
10 9 nffun 
 |-  F/ x Fun F
11 fveq2 
 |-  ( A = C -> ( F ` A ) = ( F ` C ) )
12 simplr 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> Fun F )
13 1 2 3 fliftel1 
 |-  ( ( ph /\ x e. X ) -> A F B )
14 13 ad2ant2r 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> A F B )
15 funbrfv 
 |-  ( Fun F -> ( A F B -> ( F ` A ) = B ) )
16 12 14 15 sylc 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> ( F ` A ) = B )
17 simprr 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> y e. X )
18 eqidd 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> C = C )
19 eqidd 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> D = D )
20 4 eqeq2d 
 |-  ( x = y -> ( C = A <-> C = C ) )
21 5 eqeq2d 
 |-  ( x = y -> ( D = B <-> D = D ) )
22 20 21 anbi12d 
 |-  ( x = y -> ( ( C = A /\ D = B ) <-> ( C = C /\ D = D ) ) )
23 22 rspcev 
 |-  ( ( y e. X /\ ( C = C /\ D = D ) ) -> E. x e. X ( C = A /\ D = B ) )
24 17 18 19 23 syl12anc 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> E. x e. X ( C = A /\ D = B ) )
25 1 2 3 fliftel 
 |-  ( ph -> ( C F D <-> E. x e. X ( C = A /\ D = B ) ) )
26 25 ad2antrr 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> ( C F D <-> E. x e. X ( C = A /\ D = B ) ) )
27 24 26 mpbird 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> C F D )
28 funbrfv 
 |-  ( Fun F -> ( C F D -> ( F ` C ) = D ) )
29 12 27 28 sylc 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> ( F ` C ) = D )
30 16 29 eqeq12d 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` A ) = ( F ` C ) <-> B = D ) )
31 11 30 imbitrid 
 |-  ( ( ( ph /\ Fun F ) /\ ( x e. X /\ y e. X ) ) -> ( A = C -> B = D ) )
32 31 anassrs 
 |-  ( ( ( ( ph /\ Fun F ) /\ x e. X ) /\ y e. X ) -> ( A = C -> B = D ) )
33 32 ralrimiva 
 |-  ( ( ( ph /\ Fun F ) /\ x e. X ) -> A. y e. X ( A = C -> B = D ) )
34 33 exp31 
 |-  ( ph -> ( Fun F -> ( x e. X -> A. y e. X ( A = C -> B = D ) ) ) )
35 6 10 34 ralrimd 
 |-  ( ph -> ( Fun F -> A. x e. X A. y e. X ( A = C -> B = D ) ) )
36 1 2 3 fliftel 
 |-  ( ph -> ( z F u <-> E. x e. X ( z = A /\ u = B ) ) )
37 1 2 3 fliftel 
 |-  ( ph -> ( z F v <-> E. x e. X ( z = A /\ v = B ) ) )
38 4 eqeq2d 
 |-  ( x = y -> ( z = A <-> z = C ) )
39 5 eqeq2d 
 |-  ( x = y -> ( v = B <-> v = D ) )
40 38 39 anbi12d 
 |-  ( x = y -> ( ( z = A /\ v = B ) <-> ( z = C /\ v = D ) ) )
41 40 cbvrexvw 
 |-  ( E. x e. X ( z = A /\ v = B ) <-> E. y e. X ( z = C /\ v = D ) )
42 37 41 bitrdi 
 |-  ( ph -> ( z F v <-> E. y e. X ( z = C /\ v = D ) ) )
43 36 42 anbi12d 
 |-  ( ph -> ( ( z F u /\ z F v ) <-> ( E. x e. X ( z = A /\ u = B ) /\ E. y e. X ( z = C /\ v = D ) ) ) )
44 43 biimpd 
 |-  ( ph -> ( ( z F u /\ z F v ) -> ( E. x e. X ( z = A /\ u = B ) /\ E. y e. X ( z = C /\ v = D ) ) ) )
45 reeanv 
 |-  ( E. x e. X E. y e. X ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) <-> ( E. x e. X ( z = A /\ u = B ) /\ E. y e. X ( z = C /\ v = D ) ) )
46 r19.29 
 |-  ( ( A. x e. X A. y e. X ( A = C -> B = D ) /\ E. x e. X E. y e. X ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) -> E. x e. X ( A. y e. X ( A = C -> B = D ) /\ E. y e. X ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) )
47 r19.29 
 |-  ( ( A. y e. X ( A = C -> B = D ) /\ E. y e. X ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) -> E. y e. X ( ( A = C -> B = D ) /\ ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) )
48 eqtr2 
 |-  ( ( z = A /\ z = C ) -> A = C )
49 48 ad2ant2r 
 |-  ( ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) -> A = C )
50 49 imim1i 
 |-  ( ( A = C -> B = D ) -> ( ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) -> B = D ) )
51 50 imp 
 |-  ( ( ( A = C -> B = D ) /\ ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) -> B = D )
52 simprlr 
 |-  ( ( ( A = C -> B = D ) /\ ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) -> u = B )
53 simprrr 
 |-  ( ( ( A = C -> B = D ) /\ ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) -> v = D )
54 51 52 53 3eqtr4d 
 |-  ( ( ( A = C -> B = D ) /\ ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) -> u = v )
55 54 rexlimivw 
 |-  ( E. y e. X ( ( A = C -> B = D ) /\ ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) -> u = v )
56 47 55 syl 
 |-  ( ( A. y e. X ( A = C -> B = D ) /\ E. y e. X ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) -> u = v )
57 56 rexlimivw 
 |-  ( E. x e. X ( A. y e. X ( A = C -> B = D ) /\ E. y e. X ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) -> u = v )
58 46 57 syl 
 |-  ( ( A. x e. X A. y e. X ( A = C -> B = D ) /\ E. x e. X E. y e. X ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) ) -> u = v )
59 58 ex 
 |-  ( A. x e. X A. y e. X ( A = C -> B = D ) -> ( E. x e. X E. y e. X ( ( z = A /\ u = B ) /\ ( z = C /\ v = D ) ) -> u = v ) )
60 45 59 biimtrrid 
 |-  ( A. x e. X A. y e. X ( A = C -> B = D ) -> ( ( E. x e. X ( z = A /\ u = B ) /\ E. y e. X ( z = C /\ v = D ) ) -> u = v ) )
61 44 60 syl9 
 |-  ( ph -> ( A. x e. X A. y e. X ( A = C -> B = D ) -> ( ( z F u /\ z F v ) -> u = v ) ) )
62 61 alrimdv 
 |-  ( ph -> ( A. x e. X A. y e. X ( A = C -> B = D ) -> A. v ( ( z F u /\ z F v ) -> u = v ) ) )
63 62 alrimdv 
 |-  ( ph -> ( A. x e. X A. y e. X ( A = C -> B = D ) -> A. u A. v ( ( z F u /\ z F v ) -> u = v ) ) )
64 63 alrimdv 
 |-  ( ph -> ( A. x e. X A. y e. X ( A = C -> B = D ) -> A. z A. u A. v ( ( z F u /\ z F v ) -> u = v ) ) )
65 1 2 3 fliftrel 
 |-  ( ph -> F C_ ( R X. S ) )
66 relxp 
 |-  Rel ( R X. S )
67 relss 
 |-  ( F C_ ( R X. S ) -> ( Rel ( R X. S ) -> Rel F ) )
68 65 66 67 mpisyl 
 |-  ( ph -> Rel F )
69 dffun2 
 |-  ( Fun F <-> ( Rel F /\ A. z A. u A. v ( ( z F u /\ z F v ) -> u = v ) ) )
70 69 baib 
 |-  ( Rel F -> ( Fun F <-> A. z A. u A. v ( ( z F u /\ z F v ) -> u = v ) ) )
71 68 70 syl 
 |-  ( ph -> ( Fun F <-> A. z A. u A. v ( ( z F u /\ z F v ) -> u = v ) ) )
72 64 71 sylibrd 
 |-  ( ph -> ( A. x e. X A. y e. X ( A = C -> B = D ) -> Fun F ) )
73 35 72 impbid 
 |-  ( ph -> ( Fun F <-> A. x e. X A. y e. X ( A = C -> B = D ) ) )