Metamath Proof Explorer

Theorem dssmapnvod

Description: For any base set B the duality operator for self-mappings of subsets of that base set is its own inverse, an involution. (Contributed by RP, 20-Apr-2021)

Ref Expression
Hypotheses dssmapfvd.o 
|- O = ( b e. _V |-> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) )
dssmapfvd.d 
|- D = ( O ` B )
dssmapfvd.b 
|- ( ph -> B e. V )
Assertion dssmapnvod 
|- ( ph -> `' D = D )

Proof

Step Hyp Ref Expression
1 dssmapfvd.o 
 |-  O = ( b e. _V |-> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) )
2 dssmapfvd.d 
 |-  D = ( O ` B )
3 dssmapfvd.b 
 |-  ( ph -> B e. V )
4 simpr 
 |-  ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) -> g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) )
5 difeq2 
 |-  ( s = t -> ( B \ s ) = ( B \ t ) )
6 5 fveq2d 
 |-  ( s = t -> ( f ` ( B \ s ) ) = ( f ` ( B \ t ) ) )
7 6 difeq2d 
 |-  ( s = t -> ( B \ ( f ` ( B \ s ) ) ) = ( B \ ( f ` ( B \ t ) ) ) )
8 7 cbvmptv 
 |-  ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) = ( t e. ~P B |-> ( B \ ( f ` ( B \ t ) ) ) )
9 4 8 eqtrdi 
 |-  ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) -> g = ( t e. ~P B |-> ( B \ ( f ` ( B \ t ) ) ) ) )
10 ssun1 
 |-  B C_ ( B u. ( f ` ( B \ t ) ) )
11 10 sspwi 
 |-  ~P B C_ ~P ( B u. ( f ` ( B \ t ) ) )
12 pwidg 
 |-  ( B e. V -> B e. ~P B )
13 3 12 syl 
 |-  ( ph -> B e. ~P B )
14 11 13 sseldi 
 |-  ( ph -> B e. ~P ( B u. ( f ` ( B \ t ) ) ) )
15 fvex 
 |-  ( f ` ( B \ t ) ) e. _V
16 15 elpwun 
 |-  ( B e. ~P ( B u. ( f ` ( B \ t ) ) ) <-> ( B \ ( f ` ( B \ t ) ) ) e. ~P B )
17 14 16 sylib 
 |-  ( ph -> ( B \ ( f ` ( B \ t ) ) ) e. ~P B )
18 17 ad2antrr 
 |-  ( ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( f ` ( B \ t ) ) ) e. ~P B )
19 9 18 fmpt3d 
 |-  ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) -> g : ~P B --> ~P B )
20 3 pwexd 
 |-  ( ph -> ~P B e. _V )
21 20 adantr 
 |-  ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) -> ~P B e. _V )
22 21 21 elmapd 
 |-  ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) -> ( g e. ( ~P B ^m ~P B ) <-> g : ~P B --> ~P B ) )
23 19 22 mpbird 
 |-  ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) -> g e. ( ~P B ^m ~P B ) )
24 23 adantrl 
 |-  ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) -> g e. ( ~P B ^m ~P B ) )
25 simplr 
 |-  ( ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) /\ t e. ~P B ) -> g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) )
26 difeq2 
 |-  ( s = u -> ( B \ s ) = ( B \ u ) )
27 26 fveq2d 
 |-  ( s = u -> ( f ` ( B \ s ) ) = ( f ` ( B \ u ) ) )
28 27 difeq2d 
 |-  ( s = u -> ( B \ ( f ` ( B \ s ) ) ) = ( B \ ( f ` ( B \ u ) ) ) )
29 28 cbvmptv 
 |-  ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) = ( u e. ~P B |-> ( B \ ( f ` ( B \ u ) ) ) )
30 25 29 eqtrdi 
 |-  ( ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) /\ t e. ~P B ) -> g = ( u e. ~P B |-> ( B \ ( f ` ( B \ u ) ) ) ) )
31 difeq2 
 |-  ( u = ( B \ t ) -> ( B \ u ) = ( B \ ( B \ t ) ) )
32 31 fveq2d 
 |-  ( u = ( B \ t ) -> ( f ` ( B \ u ) ) = ( f ` ( B \ ( B \ t ) ) ) )
33 32 difeq2d 
 |-  ( u = ( B \ t ) -> ( B \ ( f ` ( B \ u ) ) ) = ( B \ ( f ` ( B \ ( B \ t ) ) ) ) )
34 33 adantl 
 |-  ( ( ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) /\ t e. ~P B ) /\ u = ( B \ t ) ) -> ( B \ ( f ` ( B \ u ) ) ) = ( B \ ( f ` ( B \ ( B \ t ) ) ) ) )
35 ssun1 
 |-  B C_ ( B u. t )
36 35 sspwi 
 |-  ~P B C_ ~P ( B u. t )
37 36 13 sseldi 
 |-  ( ph -> B e. ~P ( B u. t ) )
38 vex 
 |-  t e. _V
39 38 elpwun 
 |-  ( B e. ~P ( B u. t ) <-> ( B \ t ) e. ~P B )
40 37 39 sylib 
 |-  ( ph -> ( B \ t ) e. ~P B )
41 40 ad2antrr 
 |-  ( ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
42 difexg 
 |-  ( B e. V -> ( B \ ( f ` ( B \ ( B \ t ) ) ) ) e. _V )
43 3 42 syl 
 |-  ( ph -> ( B \ ( f ` ( B \ ( B \ t ) ) ) ) e. _V )
44 43 ad2antrr 
 |-  ( ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( f ` ( B \ ( B \ t ) ) ) ) e. _V )
45 30 34 41 44 fvmptd 
 |-  ( ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) /\ t e. ~P B ) -> ( g ` ( B \ t ) ) = ( B \ ( f ` ( B \ ( B \ t ) ) ) ) )
46 45 difeq2d 
 |-  ( ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( g ` ( B \ t ) ) ) = ( B \ ( B \ ( f ` ( B \ ( B \ t ) ) ) ) ) )
47 46 adantlrl 
 |-  ( ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( g ` ( B \ t ) ) ) = ( B \ ( B \ ( f ` ( B \ ( B \ t ) ) ) ) ) )
48 elpwi 
 |-  ( t e. ~P B -> t C_ B )
49 dfss4 
 |-  ( t C_ B <-> ( B \ ( B \ t ) ) = t )
50 48 49 sylib 
 |-  ( t e. ~P B -> ( B \ ( B \ t ) ) = t )
51 50 fveq2d 
 |-  ( t e. ~P B -> ( f ` ( B \ ( B \ t ) ) ) = ( f ` t ) )
52 51 difeq2d 
 |-  ( t e. ~P B -> ( B \ ( f ` ( B \ ( B \ t ) ) ) ) = ( B \ ( f ` t ) ) )
53 52 difeq2d 
 |-  ( t e. ~P B -> ( B \ ( B \ ( f ` ( B \ ( B \ t ) ) ) ) ) = ( B \ ( B \ ( f ` t ) ) ) )
54 53 adantl 
 |-  ( ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( B \ ( f ` ( B \ ( B \ t ) ) ) ) ) = ( B \ ( B \ ( f ` t ) ) ) )
55 20 20 elmapd 
 |-  ( ph -> ( f e. ( ~P B ^m ~P B ) <-> f : ~P B --> ~P B ) )
56 55 biimpa 
 |-  ( ( ph /\ f e. ( ~P B ^m ~P B ) ) -> f : ~P B --> ~P B )
57 56 ffvelrnda 
 |-  ( ( ( ph /\ f e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( f ` t ) e. ~P B )
58 57 elpwid 
 |-  ( ( ( ph /\ f e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( f ` t ) C_ B )
59 dfss4 
 |-  ( ( f ` t ) C_ B <-> ( B \ ( B \ ( f ` t ) ) ) = ( f ` t ) )
60 58 59 sylib 
 |-  ( ( ( ph /\ f e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( B \ ( B \ ( f ` t ) ) ) = ( f ` t ) )
61 60 adantlrr 
 |-  ( ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( B \ ( f ` t ) ) ) = ( f ` t ) )
62 47 54 61 3eqtrrd 
 |-  ( ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) /\ t e. ~P B ) -> ( f ` t ) = ( B \ ( g ` ( B \ t ) ) ) )
63 62 ralrimiva 
 |-  ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) -> A. t e. ~P B ( f ` t ) = ( B \ ( g ` ( B \ t ) ) ) )
64 elmapfn 
 |-  ( f e. ( ~P B ^m ~P B ) -> f Fn ~P B )
65 64 ad2antrl 
 |-  ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) -> f Fn ~P B )
66 difeq2 
 |-  ( t = z -> ( B \ t ) = ( B \ z ) )
67 66 fveq2d 
 |-  ( t = z -> ( g ` ( B \ t ) ) = ( g ` ( B \ z ) ) )
68 67 difeq2d 
 |-  ( t = z -> ( B \ ( g ` ( B \ t ) ) ) = ( B \ ( g ` ( B \ z ) ) ) )
69 difexg 
 |-  ( B e. V -> ( B \ ( g ` ( B \ t ) ) ) e. _V )
70 3 69 syl 
 |-  ( ph -> ( B \ ( g ` ( B \ t ) ) ) e. _V )
71 70 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( g ` ( B \ t ) ) ) e. _V )
72 difexg 
 |-  ( B e. V -> ( B \ ( g ` ( B \ z ) ) ) e. _V )
73 3 72 syl 
 |-  ( ph -> ( B \ ( g ` ( B \ z ) ) ) e. _V )
74 73 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) /\ z e. ~P B ) -> ( B \ ( g ` ( B \ z ) ) ) e. _V )
75 65 68 71 74 fnmptfvd 
 |-  ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) -> ( f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) <-> A. t e. ~P B ( f ` t ) = ( B \ ( g ` ( B \ t ) ) ) ) )
76 63 75 mpbird 
 |-  ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) -> f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) )
77 24 76 jca 
 |-  ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) -> ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) )
78 simpr 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) )
79 difeq2 
 |-  ( z = t -> ( B \ z ) = ( B \ t ) )
80 79 fveq2d 
 |-  ( z = t -> ( g ` ( B \ z ) ) = ( g ` ( B \ t ) ) )
81 80 difeq2d 
 |-  ( z = t -> ( B \ ( g ` ( B \ z ) ) ) = ( B \ ( g ` ( B \ t ) ) ) )
82 81 cbvmptv 
 |-  ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) = ( t e. ~P B |-> ( B \ ( g ` ( B \ t ) ) ) )
83 78 82 eqtrdi 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> f = ( t e. ~P B |-> ( B \ ( g ` ( B \ t ) ) ) ) )
84 ssun1 
 |-  B C_ ( B u. ( g ` ( B \ t ) ) )
85 84 sspwi 
 |-  ~P B C_ ~P ( B u. ( g ` ( B \ t ) ) )
86 85 13 sseldi 
 |-  ( ph -> B e. ~P ( B u. ( g ` ( B \ t ) ) ) )
87 fvex 
 |-  ( g ` ( B \ t ) ) e. _V
88 87 elpwun 
 |-  ( B e. ~P ( B u. ( g ` ( B \ t ) ) ) <-> ( B \ ( g ` ( B \ t ) ) ) e. ~P B )
89 86 88 sylib 
 |-  ( ph -> ( B \ ( g ` ( B \ t ) ) ) e. ~P B )
90 89 ad2antrr 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( g ` ( B \ t ) ) ) e. ~P B )
91 83 90 fmpt3d 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> f : ~P B --> ~P B )
92 20 adantr 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> ~P B e. _V )
93 92 92 elmapd 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> ( f e. ( ~P B ^m ~P B ) <-> f : ~P B --> ~P B ) )
94 91 93 mpbird 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> f e. ( ~P B ^m ~P B ) )
95 94 adantrl 
 |-  ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) -> f e. ( ~P B ^m ~P B ) )
96 simplr 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) )
97 difeq2 
 |-  ( z = u -> ( B \ z ) = ( B \ u ) )
98 97 fveq2d 
 |-  ( z = u -> ( g ` ( B \ z ) ) = ( g ` ( B \ u ) ) )
99 98 difeq2d 
 |-  ( z = u -> ( B \ ( g ` ( B \ z ) ) ) = ( B \ ( g ` ( B \ u ) ) ) )
100 99 cbvmptv 
 |-  ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) = ( u e. ~P B |-> ( B \ ( g ` ( B \ u ) ) ) )
101 96 100 eqtrdi 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> f = ( u e. ~P B |-> ( B \ ( g ` ( B \ u ) ) ) ) )
102 31 fveq2d 
 |-  ( u = ( B \ t ) -> ( g ` ( B \ u ) ) = ( g ` ( B \ ( B \ t ) ) ) )
103 102 difeq2d 
 |-  ( u = ( B \ t ) -> ( B \ ( g ` ( B \ u ) ) ) = ( B \ ( g ` ( B \ ( B \ t ) ) ) ) )
104 103 adantl 
 |-  ( ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) /\ u = ( B \ t ) ) -> ( B \ ( g ` ( B \ u ) ) ) = ( B \ ( g ` ( B \ ( B \ t ) ) ) ) )
105 40 ad2antrr 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
106 difexg 
 |-  ( B e. V -> ( B \ ( g ` ( B \ ( B \ t ) ) ) ) e. _V )
107 3 106 syl 
 |-  ( ph -> ( B \ ( g ` ( B \ ( B \ t ) ) ) ) e. _V )
108 107 ad2antrr 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( g ` ( B \ ( B \ t ) ) ) ) e. _V )
109 101 104 105 108 fvmptd 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> ( f ` ( B \ t ) ) = ( B \ ( g ` ( B \ ( B \ t ) ) ) ) )
110 109 difeq2d 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( f ` ( B \ t ) ) ) = ( B \ ( B \ ( g ` ( B \ ( B \ t ) ) ) ) ) )
111 110 adantlrl 
 |-  ( ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( f ` ( B \ t ) ) ) = ( B \ ( B \ ( g ` ( B \ ( B \ t ) ) ) ) ) )
112 50 fveq2d 
 |-  ( t e. ~P B -> ( g ` ( B \ ( B \ t ) ) ) = ( g ` t ) )
113 112 difeq2d 
 |-  ( t e. ~P B -> ( B \ ( g ` ( B \ ( B \ t ) ) ) ) = ( B \ ( g ` t ) ) )
114 113 difeq2d 
 |-  ( t e. ~P B -> ( B \ ( B \ ( g ` ( B \ ( B \ t ) ) ) ) ) = ( B \ ( B \ ( g ` t ) ) ) )
115 114 adantl 
 |-  ( ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( B \ ( g ` ( B \ ( B \ t ) ) ) ) ) = ( B \ ( B \ ( g ` t ) ) ) )
116 20 20 elmapd 
 |-  ( ph -> ( g e. ( ~P B ^m ~P B ) <-> g : ~P B --> ~P B ) )
117 116 biimpa 
 |-  ( ( ph /\ g e. ( ~P B ^m ~P B ) ) -> g : ~P B --> ~P B )
118 117 ffvelrnda 
 |-  ( ( ( ph /\ g e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( g ` t ) e. ~P B )
119 118 elpwid 
 |-  ( ( ( ph /\ g e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( g ` t ) C_ B )
120 dfss4 
 |-  ( ( g ` t ) C_ B <-> ( B \ ( B \ ( g ` t ) ) ) = ( g ` t ) )
121 119 120 sylib 
 |-  ( ( ( ph /\ g e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( B \ ( B \ ( g ` t ) ) ) = ( g ` t ) )
122 121 adantlrr 
 |-  ( ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( B \ ( g ` t ) ) ) = ( g ` t ) )
123 111 115 122 3eqtrrd 
 |-  ( ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) /\ t e. ~P B ) -> ( g ` t ) = ( B \ ( f ` ( B \ t ) ) ) )
124 123 ralrimiva 
 |-  ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) -> A. t e. ~P B ( g ` t ) = ( B \ ( f ` ( B \ t ) ) ) )
125 elmapfn 
 |-  ( g e. ( ~P B ^m ~P B ) -> g Fn ~P B )
126 125 ad2antrl 
 |-  ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) -> g Fn ~P B )
127 difeq2 
 |-  ( t = s -> ( B \ t ) = ( B \ s ) )
128 127 fveq2d 
 |-  ( t = s -> ( f ` ( B \ t ) ) = ( f ` ( B \ s ) ) )
129 128 difeq2d 
 |-  ( t = s -> ( B \ ( f ` ( B \ t ) ) ) = ( B \ ( f ` ( B \ s ) ) ) )
130 difexg 
 |-  ( B e. V -> ( B \ ( f ` ( B \ t ) ) ) e. _V )
131 3 130 syl 
 |-  ( ph -> ( B \ ( f ` ( B \ t ) ) ) e. _V )
132 131 ad2antrr 
 |-  ( ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( f ` ( B \ t ) ) ) e. _V )
133 difexg 
 |-  ( B e. V -> ( B \ ( f ` ( B \ s ) ) ) e. _V )
134 3 133 syl 
 |-  ( ph -> ( B \ ( f ` ( B \ s ) ) ) e. _V )
135 134 ad2antrr 
 |-  ( ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) /\ s e. ~P B ) -> ( B \ ( f ` ( B \ s ) ) ) e. _V )
136 126 129 132 135 fnmptfvd 
 |-  ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) -> ( g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) <-> A. t e. ~P B ( g ` t ) = ( B \ ( f ` ( B \ t ) ) ) ) )
137 124 136 mpbird 
 |-  ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) -> g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) )
138 95 137 jca 
 |-  ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) -> ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )
139 77 138 impbida 
 |-  ( ph -> ( ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) <-> ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) )
140 139 mptcnv 
 |-  ( ph -> `' ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) = ( g e. ( ~P B ^m ~P B ) |-> ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) )
141 1 2 3 dssmapfvd 
 |-  ( ph -> D = ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )
142 141 cnveqd 
 |-  ( ph -> `' D = `' ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )
143 fveq1 
 |-  ( f = g -> ( f ` ( b \ s ) ) = ( g ` ( b \ s ) ) )
144 143 difeq2d 
 |-  ( f = g -> ( b \ ( f ` ( b \ s ) ) ) = ( b \ ( g ` ( b \ s ) ) ) )
145 144 mpteq2dv 
 |-  ( f = g -> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) = ( s e. ~P b |-> ( b \ ( g ` ( b \ s ) ) ) ) )
146 difeq2 
 |-  ( s = z -> ( b \ s ) = ( b \ z ) )
147 146 fveq2d 
 |-  ( s = z -> ( g ` ( b \ s ) ) = ( g ` ( b \ z ) ) )
148 147 difeq2d 
 |-  ( s = z -> ( b \ ( g ` ( b \ s ) ) ) = ( b \ ( g ` ( b \ z ) ) ) )
149 148 cbvmptv 
 |-  ( s e. ~P b |-> ( b \ ( g ` ( b \ s ) ) ) ) = ( z e. ~P b |-> ( b \ ( g ` ( b \ z ) ) ) )
150 145 149 eqtrdi 
 |-  ( f = g -> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) = ( z e. ~P b |-> ( b \ ( g ` ( b \ z ) ) ) ) )
151 150 cbvmptv 
 |-  ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) = ( g e. ( ~P b ^m ~P b ) |-> ( z e. ~P b |-> ( b \ ( g ` ( b \ z ) ) ) ) )
152 151 mpteq2i 
 |-  ( b e. _V |-> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) ) = ( b e. _V |-> ( g e. ( ~P b ^m ~P b ) |-> ( z e. ~P b |-> ( b \ ( g ` ( b \ z ) ) ) ) ) )
153 1 152 eqtri 
 |-  O = ( b e. _V |-> ( g e. ( ~P b ^m ~P b ) |-> ( z e. ~P b |-> ( b \ ( g ` ( b \ z ) ) ) ) ) )
154 153 2 3 dssmapfvd 
 |-  ( ph -> D = ( g e. ( ~P B ^m ~P B ) |-> ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) )
155 140 142 154 3eqtr4d 
 |-  ( ph -> `' D = D )