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

Metamath Proof Explorer

Theorem fliftf

Description: The domain and range 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 )
Assertion fliftf 
|- ( ph -> ( Fun F <-> F : ran ( x e. X |-> A ) --> S ) )

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 simpr 
 |-  ( ( ph /\ Fun F ) -> Fun F )
5 1 2 3 fliftel 
 |-  ( ph -> ( y F z <-> E. x e. X ( y = A /\ z = B ) ) )
6 5 exbidv 
 |-  ( ph -> ( E. z y F z <-> E. z E. x e. X ( y = A /\ z = B ) ) )
7 6 adantr 
 |-  ( ( ph /\ Fun F ) -> ( E. z y F z <-> E. z E. x e. X ( y = A /\ z = B ) ) )
8 rexcom4 
 |-  ( E. x e. X E. z ( y = A /\ z = B ) <-> E. z E. x e. X ( y = A /\ z = B ) )
9 19.42v 
 |-  ( E. z ( y = A /\ z = B ) <-> ( y = A /\ E. z z = B ) )
10 elisset 
 |-  ( B e. S -> E. z z = B )
11 3 10 syl 
 |-  ( ( ph /\ x e. X ) -> E. z z = B )
12 11 biantrud 
 |-  ( ( ph /\ x e. X ) -> ( y = A <-> ( y = A /\ E. z z = B ) ) )
13 9 12 bitr4id 
 |-  ( ( ph /\ x e. X ) -> ( E. z ( y = A /\ z = B ) <-> y = A ) )
14 13 rexbidva 
 |-  ( ph -> ( E. x e. X E. z ( y = A /\ z = B ) <-> E. x e. X y = A ) )
15 14 adantr 
 |-  ( ( ph /\ Fun F ) -> ( E. x e. X E. z ( y = A /\ z = B ) <-> E. x e. X y = A ) )
16 8 15 bitr3id 
 |-  ( ( ph /\ Fun F ) -> ( E. z E. x e. X ( y = A /\ z = B ) <-> E. x e. X y = A ) )
17 7 16 bitrd 
 |-  ( ( ph /\ Fun F ) -> ( E. z y F z <-> E. x e. X y = A ) )
18 17 abbidv 
 |-  ( ( ph /\ Fun F ) -> { y | E. z y F z } = { y | E. x e. X y = A } )
19 df-dm 
 |-  dom F = { y | E. z y F z }
20 eqid 
 |-  ( x e. X |-> A ) = ( x e. X |-> A )
21 20 rnmpt 
 |-  ran ( x e. X |-> A ) = { y | E. x e. X y = A }
22 18 19 21 3eqtr4g 
 |-  ( ( ph /\ Fun F ) -> dom F = ran ( x e. X |-> A ) )
23 df-fn 
 |-  ( F Fn ran ( x e. X |-> A ) <-> ( Fun F /\ dom F = ran ( x e. X |-> A ) ) )
24 4 22 23 sylanbrc 
 |-  ( ( ph /\ Fun F ) -> F Fn ran ( x e. X |-> A ) )
25 1 2 3 fliftrel 
 |-  ( ph -> F C_ ( R X. S ) )
26 25 adantr 
 |-  ( ( ph /\ Fun F ) -> F C_ ( R X. S ) )
27 rnss 
 |-  ( F C_ ( R X. S ) -> ran F C_ ran ( R X. S ) )
28 26 27 syl 
 |-  ( ( ph /\ Fun F ) -> ran F C_ ran ( R X. S ) )
29 rnxpss 
 |-  ran ( R X. S ) C_ S
30 28 29 sstrdi 
 |-  ( ( ph /\ Fun F ) -> ran F C_ S )
31 df-f 
 |-  ( F : ran ( x e. X |-> A ) --> S <-> ( F Fn ran ( x e. X |-> A ) /\ ran F C_ S ) )
32 24 30 31 sylanbrc 
 |-  ( ( ph /\ Fun F ) -> F : ran ( x e. X |-> A ) --> S )
33 32 ex 
 |-  ( ph -> ( Fun F -> F : ran ( x e. X |-> A ) --> S ) )
34 ffun 
 |-  ( F : ran ( x e. X |-> A ) --> S -> Fun F )
35 33 34 impbid1 
 |-  ( ph -> ( Fun F <-> F : ran ( x e. X |-> A ) --> S ) )