This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fliftval

Description: The value of the function F . (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 )
fliftval.4 
|- ( x = Y -> A = C )
fliftval.5 
|- ( x = Y -> B = D )
fliftval.6 
|- ( ph -> Fun F )
Assertion fliftval 
|- ( ( ph /\ Y e. X ) -> ( F ` C ) = 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 fliftval.4 
 |-  ( x = Y -> A = C )
5 fliftval.5 
 |-  ( x = Y -> B = D )
6 fliftval.6 
 |-  ( ph -> Fun F )
7 6 adantr 
 |-  ( ( ph /\ Y e. X ) -> Fun F )
8 simpr 
 |-  ( ( ph /\ Y e. X ) -> Y e. X )
9 eqidd 
 |-  ( ph -> D = D )
10 eqidd 
 |-  ( Y e. X -> C = C )
11 9 10 anim12ci 
 |-  ( ( ph /\ Y e. X ) -> ( C = C /\ D = D ) )
12 4 eqeq2d 
 |-  ( x = Y -> ( C = A <-> C = C ) )
13 5 eqeq2d 
 |-  ( x = Y -> ( D = B <-> D = D ) )
14 12 13 anbi12d 
 |-  ( x = Y -> ( ( C = A /\ D = B ) <-> ( C = C /\ D = D ) ) )
15 14 rspcev 
 |-  ( ( Y e. X /\ ( C = C /\ D = D ) ) -> E. x e. X ( C = A /\ D = B ) )
16 8 11 15 syl2anc 
 |-  ( ( ph /\ Y e. X ) -> E. x e. X ( C = A /\ D = B ) )
17 1 2 3 fliftel 
 |-  ( ph -> ( C F D <-> E. x e. X ( C = A /\ D = B ) ) )
18 17 adantr 
 |-  ( ( ph /\ Y e. X ) -> ( C F D <-> E. x e. X ( C = A /\ D = B ) ) )
19 16 18 mpbird 
 |-  ( ( ph /\ Y e. X ) -> C F D )
20 funbrfv 
 |-  ( Fun F -> ( C F D -> ( F ` C ) = D ) )
21 7 19 20 sylc 
 |-  ( ( ph /\ Y e. X ) -> ( F ` C ) = D )