Metamath Proof Explorer

Theorem mptcnfimad

Description: The converse of a mapping of subsets to their image of a bijection. (Contributed by AV, 23-Apr-2025)

Ref Expression
Hypotheses mptcnfimad.m 
|- M = ( x e. A |-> ( F " x ) )
mptcnfimad.f 
|- ( ph -> F : V -1-1-onto-> W )
mptcnfimad.a 
|- ( ph -> A C_ ~P V )
mptcnfimad.r 
|- ( ph -> ran M C_ ~P W )
mptcnfimad.v 
|- ( ph -> V e. U )
Assertion mptcnfimad 
|- ( ph -> `' M = ( y e. ran M |-> ( `' F " y ) ) )

Proof

Step Hyp Ref Expression
1 mptcnfimad.m 
 |-  M = ( x e. A |-> ( F " x ) )
2 mptcnfimad.f 
 |-  ( ph -> F : V -1-1-onto-> W )
3 mptcnfimad.a 
 |-  ( ph -> A C_ ~P V )
4 mptcnfimad.r 
 |-  ( ph -> ran M C_ ~P W )
5 mptcnfimad.v 
 |-  ( ph -> V e. U )
6 1 cnveqi 
 |-  `' M = `' ( x e. A |-> ( F " x ) )
7 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
8 f1of 
 |-  ( F : V -1-1-onto-> W -> F : V --> W )
9 2 8 syl 
 |-  ( ph -> F : V --> W )
10 9 5 fexd 
 |-  ( ph -> F e. _V )
11 10 imaexd 
 |-  ( ph -> ( F " x ) e. _V )
12 11 adantr 
 |-  ( ( ph /\ x e. A ) -> ( F " x ) e. _V )
13 1 7 12 elrnmpt1d 
 |-  ( ( ph /\ x e. A ) -> ( F " x ) e. ran M )
14 f1of1 
 |-  ( F : V -1-1-onto-> W -> F : V -1-1-> W )
15 2 14 syl 
 |-  ( ph -> F : V -1-1-> W )
16 ssel 
 |-  ( A C_ ~P V -> ( x e. A -> x e. ~P V ) )
17 elpwi 
 |-  ( x e. ~P V -> x C_ V )
18 16 17 syl6 
 |-  ( A C_ ~P V -> ( x e. A -> x C_ V ) )
19 3 18 syl 
 |-  ( ph -> ( x e. A -> x C_ V ) )
20 19 imp 
 |-  ( ( ph /\ x e. A ) -> x C_ V )
21 f1imacnv 
 |-  ( ( F : V -1-1-> W /\ x C_ V ) -> ( `' F " ( F " x ) ) = x )
22 21 eqcomd 
 |-  ( ( F : V -1-1-> W /\ x C_ V ) -> x = ( `' F " ( F " x ) ) )
23 15 20 22 syl2an2r 
 |-  ( ( ph /\ x e. A ) -> x = ( `' F " ( F " x ) ) )
24 13 23 jca 
 |-  ( ( ph /\ x e. A ) -> ( ( F " x ) e. ran M /\ x = ( `' F " ( F " x ) ) ) )
25 eleq1 
 |-  ( y = ( F " x ) -> ( y e. ran M <-> ( F " x ) e. ran M ) )
26 imaeq2 
 |-  ( y = ( F " x ) -> ( `' F " y ) = ( `' F " ( F " x ) ) )
27 26 eqeq2d 
 |-  ( y = ( F " x ) -> ( x = ( `' F " y ) <-> x = ( `' F " ( F " x ) ) ) )
28 25 27 anbi12d 
 |-  ( y = ( F " x ) -> ( ( y e. ran M /\ x = ( `' F " y ) ) <-> ( ( F " x ) e. ran M /\ x = ( `' F " ( F " x ) ) ) ) )
29 24 28 syl5ibrcom 
 |-  ( ( ph /\ x e. A ) -> ( y = ( F " x ) -> ( y e. ran M /\ x = ( `' F " y ) ) ) )
30 29 expimpd 
 |-  ( ph -> ( ( x e. A /\ y = ( F " x ) ) -> ( y e. ran M /\ x = ( `' F " y ) ) ) )
31 12 ralrimiva 
 |-  ( ph -> A. x e. A ( F " x ) e. _V )
32 1 fnmpt 
 |-  ( A. x e. A ( F " x ) e. _V -> M Fn A )
33 31 32 syl 
 |-  ( ph -> M Fn A )
34 fvelrnb 
 |-  ( M Fn A -> ( y e. ran M <-> E. x e. A ( M ` x ) = y ) )
35 33 34 syl 
 |-  ( ph -> ( y e. ran M <-> E. x e. A ( M ` x ) = y ) )
36 imaeq2 
 |-  ( x = z -> ( F " x ) = ( F " z ) )
37 36 cbvmptv 
 |-  ( x e. A |-> ( F " x ) ) = ( z e. A |-> ( F " z ) )
38 1 37 eqtri 
 |-  M = ( z e. A |-> ( F " z ) )
39 38 a1i 
 |-  ( ( ph /\ x e. A ) -> M = ( z e. A |-> ( F " z ) ) )
40 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ z = x ) -> z = x )
41 40 imaeq2d 
 |-  ( ( ( ph /\ x e. A ) /\ z = x ) -> ( F " z ) = ( F " x ) )
42 39 41 7 12 fvmptd 
 |-  ( ( ph /\ x e. A ) -> ( M ` x ) = ( F " x ) )
43 42 eqeq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( M ` x ) = y <-> ( F " x ) = y ) )
44 26 eqcoms 
 |-  ( ( F " x ) = y -> ( `' F " y ) = ( `' F " ( F " x ) ) )
45 44 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ ( F " x ) = y ) -> ( `' F " y ) = ( `' F " ( F " x ) ) )
46 15 20 21 syl2an2r 
 |-  ( ( ph /\ x e. A ) -> ( `' F " ( F " x ) ) = x )
47 46 7 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> ( `' F " ( F " x ) ) e. A )
48 47 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ ( F " x ) = y ) -> ( `' F " ( F " x ) ) e. A )
49 45 48 eqeltrd 
 |-  ( ( ( ph /\ x e. A ) /\ ( F " x ) = y ) -> ( `' F " y ) e. A )
50 49 ex 
 |-  ( ( ph /\ x e. A ) -> ( ( F " x ) = y -> ( `' F " y ) e. A ) )
51 43 50 sylbid 
 |-  ( ( ph /\ x e. A ) -> ( ( M ` x ) = y -> ( `' F " y ) e. A ) )
52 51 rexlimdva 
 |-  ( ph -> ( E. x e. A ( M ` x ) = y -> ( `' F " y ) e. A ) )
53 35 52 sylbid 
 |-  ( ph -> ( y e. ran M -> ( `' F " y ) e. A ) )
54 53 imp 
 |-  ( ( ph /\ y e. ran M ) -> ( `' F " y ) e. A )
55 f1ofo 
 |-  ( F : V -1-1-onto-> W -> F : V -onto-> W )
56 2 55 syl 
 |-  ( ph -> F : V -onto-> W )
57 ssel 
 |-  ( ran M C_ ~P W -> ( y e. ran M -> y e. ~P W ) )
58 elpwi 
 |-  ( y e. ~P W -> y C_ W )
59 57 58 syl6 
 |-  ( ran M C_ ~P W -> ( y e. ran M -> y C_ W ) )
60 4 59 syl 
 |-  ( ph -> ( y e. ran M -> y C_ W ) )
61 60 imp 
 |-  ( ( ph /\ y e. ran M ) -> y C_ W )
62 foimacnv 
 |-  ( ( F : V -onto-> W /\ y C_ W ) -> ( F " ( `' F " y ) ) = y )
63 56 61 62 syl2an2r 
 |-  ( ( ph /\ y e. ran M ) -> ( F " ( `' F " y ) ) = y )
64 63 eqcomd 
 |-  ( ( ph /\ y e. ran M ) -> y = ( F " ( `' F " y ) ) )
65 54 64 jca 
 |-  ( ( ph /\ y e. ran M ) -> ( ( `' F " y ) e. A /\ y = ( F " ( `' F " y ) ) ) )
66 eleq1 
 |-  ( x = ( `' F " y ) -> ( x e. A <-> ( `' F " y ) e. A ) )
67 imaeq2 
 |-  ( x = ( `' F " y ) -> ( F " x ) = ( F " ( `' F " y ) ) )
68 67 eqeq2d 
 |-  ( x = ( `' F " y ) -> ( y = ( F " x ) <-> y = ( F " ( `' F " y ) ) ) )
69 66 68 anbi12d 
 |-  ( x = ( `' F " y ) -> ( ( x e. A /\ y = ( F " x ) ) <-> ( ( `' F " y ) e. A /\ y = ( F " ( `' F " y ) ) ) ) )
70 65 69 syl5ibrcom 
 |-  ( ( ph /\ y e. ran M ) -> ( x = ( `' F " y ) -> ( x e. A /\ y = ( F " x ) ) ) )
71 70 expimpd 
 |-  ( ph -> ( ( y e. ran M /\ x = ( `' F " y ) ) -> ( x e. A /\ y = ( F " x ) ) ) )
72 30 71 impbid 
 |-  ( ph -> ( ( x e. A /\ y = ( F " x ) ) <-> ( y e. ran M /\ x = ( `' F " y ) ) ) )
73 72 mptcnv 
 |-  ( ph -> `' ( x e. A |-> ( F " x ) ) = ( y e. ran M |-> ( `' F " y ) ) )
74 6 73 eqtrid 
 |-  ( ph -> `' M = ( y e. ran M |-> ( `' F " y ) ) )