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 sselid 
 |-  ( 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 sselid 
 |-  ( 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 3 difexd 
 |-  ( ph -> ( B \ ( f ` ( B \ ( B \ t ) ) ) ) e. _V )
43 42 ad2antrr 
 |-  ( ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( f ` ( B \ ( B \ t ) ) ) ) e. _V )
44 30 34 41 43 fvmptd 
 |-  ( ( ( ph /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) /\ t e. ~P B ) -> ( g ` ( B \ t ) ) = ( B \ ( f ` ( B \ ( B \ t ) ) ) ) )
45 44 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 ) ) ) ) ) )
46 45 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 ) ) ) ) ) )
47 elpwi 
 |-  ( t e. ~P B -> t C_ B )
48 dfss4 
 |-  ( t C_ B <-> ( B \ ( B \ t ) ) = t )
49 47 48 sylib 
 |-  ( t e. ~P B -> ( B \ ( B \ t ) ) = t )
50 49 fveq2d 
 |-  ( t e. ~P B -> ( f ` ( B \ ( B \ t ) ) ) = ( f ` t ) )
51 50 difeq2d 
 |-  ( t e. ~P B -> ( B \ ( f ` ( B \ ( B \ t ) ) ) ) = ( B \ ( f ` t ) ) )
52 51 difeq2d 
 |-  ( t e. ~P B -> ( B \ ( B \ ( f ` ( B \ ( B \ t ) ) ) ) ) = ( B \ ( B \ ( f ` t ) ) ) )
53 52 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 ) ) ) )
54 20 20 elmapd 
 |-  ( ph -> ( f e. ( ~P B ^m ~P B ) <-> f : ~P B --> ~P B ) )
55 54 biimpa 
 |-  ( ( ph /\ f e. ( ~P B ^m ~P B ) ) -> f : ~P B --> ~P B )
56 55 ffvelcdmda 
 |-  ( ( ( ph /\ f e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( f ` t ) e. ~P B )
57 56 elpwid 
 |-  ( ( ( ph /\ f e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( f ` t ) C_ B )
58 dfss4 
 |-  ( ( f ` t ) C_ B <-> ( B \ ( B \ ( f ` t ) ) ) = ( f ` t ) )
59 57 58 sylib 
 |-  ( ( ( ph /\ f e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( B \ ( B \ ( f ` t ) ) ) = ( f ` t ) )
60 59 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 ) )
61 46 53 60 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 ) ) ) )
62 61 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 ) ) ) )
63 elmapfn 
 |-  ( f e. ( ~P B ^m ~P B ) -> f Fn ~P B )
64 63 ad2antrl 
 |-  ( ( ph /\ ( f e. ( ~P B ^m ~P B ) /\ g = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) ) -> f Fn ~P B )
65 difeq2 
 |-  ( t = z -> ( B \ t ) = ( B \ z ) )
66 65 fveq2d 
 |-  ( t = z -> ( g ` ( B \ t ) ) = ( g ` ( B \ z ) ) )
67 66 difeq2d 
 |-  ( t = z -> ( B \ ( g ` ( B \ t ) ) ) = ( B \ ( g ` ( B \ z ) ) ) )
68 3 difexd 
 |-  ( ph -> ( B \ ( g ` ( B \ t ) ) ) e. _V )
69 68 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 )
70 3 difexd 
 |-  ( ph -> ( B \ ( g ` ( B \ z ) ) ) e. _V )
71 70 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 )
72 64 67 69 71 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 ) ) ) ) )
73 62 72 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 ) ) ) ) )
74 24 73 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 ) ) ) ) ) )
75 simpr 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) )
76 difeq2 
 |-  ( z = t -> ( B \ z ) = ( B \ t ) )
77 76 fveq2d 
 |-  ( z = t -> ( g ` ( B \ z ) ) = ( g ` ( B \ t ) ) )
78 77 difeq2d 
 |-  ( z = t -> ( B \ ( g ` ( B \ z ) ) ) = ( B \ ( g ` ( B \ t ) ) ) )
79 78 cbvmptv 
 |-  ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) = ( t e. ~P B |-> ( B \ ( g ` ( B \ t ) ) ) )
80 75 79 eqtrdi 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> f = ( t e. ~P B |-> ( B \ ( g ` ( B \ t ) ) ) ) )
81 ssun1 
 |-  B C_ ( B u. ( g ` ( B \ t ) ) )
82 81 sspwi 
 |-  ~P B C_ ~P ( B u. ( g ` ( B \ t ) ) )
83 82 13 sselid 
 |-  ( ph -> B e. ~P ( B u. ( g ` ( B \ t ) ) ) )
84 fvex 
 |-  ( g ` ( B \ t ) ) e. _V
85 84 elpwun 
 |-  ( B e. ~P ( B u. ( g ` ( B \ t ) ) ) <-> ( B \ ( g ` ( B \ t ) ) ) e. ~P B )
86 83 85 sylib 
 |-  ( ph -> ( B \ ( g ` ( B \ t ) ) ) e. ~P B )
87 86 ad2antrr 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( g ` ( B \ t ) ) ) e. ~P B )
88 80 87 fmpt3d 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> f : ~P B --> ~P B )
89 20 adantr 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> ~P B e. _V )
90 89 89 elmapd 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> ( f e. ( ~P B ^m ~P B ) <-> f : ~P B --> ~P B ) )
91 88 90 mpbird 
 |-  ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) -> f e. ( ~P B ^m ~P B ) )
92 91 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 ) )
93 simplr 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) )
94 difeq2 
 |-  ( z = u -> ( B \ z ) = ( B \ u ) )
95 94 fveq2d 
 |-  ( z = u -> ( g ` ( B \ z ) ) = ( g ` ( B \ u ) ) )
96 95 difeq2d 
 |-  ( z = u -> ( B \ ( g ` ( B \ z ) ) ) = ( B \ ( g ` ( B \ u ) ) ) )
97 96 cbvmptv 
 |-  ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) = ( u e. ~P B |-> ( B \ ( g ` ( B \ u ) ) ) )
98 93 97 eqtrdi 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> f = ( u e. ~P B |-> ( B \ ( g ` ( B \ u ) ) ) ) )
99 31 fveq2d 
 |-  ( u = ( B \ t ) -> ( g ` ( B \ u ) ) = ( g ` ( B \ ( B \ t ) ) ) )
100 99 difeq2d 
 |-  ( u = ( B \ t ) -> ( B \ ( g ` ( B \ u ) ) ) = ( B \ ( g ` ( B \ ( B \ t ) ) ) ) )
101 100 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 ) ) ) ) )
102 40 ad2antrr 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
103 3 difexd 
 |-  ( ph -> ( B \ ( g ` ( B \ ( B \ t ) ) ) ) e. _V )
104 103 ad2antrr 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> ( B \ ( g ` ( B \ ( B \ t ) ) ) ) e. _V )
105 98 101 102 104 fvmptd 
 |-  ( ( ( ph /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) /\ t e. ~P B ) -> ( f ` ( B \ t ) ) = ( B \ ( g ` ( B \ ( B \ t ) ) ) ) )
106 105 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 ) ) ) ) ) )
107 106 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 ) ) ) ) ) )
108 49 fveq2d 
 |-  ( t e. ~P B -> ( g ` ( B \ ( B \ t ) ) ) = ( g ` t ) )
109 108 difeq2d 
 |-  ( t e. ~P B -> ( B \ ( g ` ( B \ ( B \ t ) ) ) ) = ( B \ ( g ` t ) ) )
110 109 difeq2d 
 |-  ( t e. ~P B -> ( B \ ( B \ ( g ` ( B \ ( B \ t ) ) ) ) ) = ( B \ ( B \ ( g ` t ) ) ) )
111 110 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 ) ) ) )
112 20 20 elmapd 
 |-  ( ph -> ( g e. ( ~P B ^m ~P B ) <-> g : ~P B --> ~P B ) )
113 112 biimpa 
 |-  ( ( ph /\ g e. ( ~P B ^m ~P B ) ) -> g : ~P B --> ~P B )
114 113 ffvelcdmda 
 |-  ( ( ( ph /\ g e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( g ` t ) e. ~P B )
115 114 elpwid 
 |-  ( ( ( ph /\ g e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( g ` t ) C_ B )
116 dfss4 
 |-  ( ( g ` t ) C_ B <-> ( B \ ( B \ ( g ` t ) ) ) = ( g ` t ) )
117 115 116 sylib 
 |-  ( ( ( ph /\ g e. ( ~P B ^m ~P B ) ) /\ t e. ~P B ) -> ( B \ ( B \ ( g ` t ) ) ) = ( g ` t ) )
118 117 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 ) )
119 107 111 118 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 ) ) ) )
120 119 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 ) ) ) )
121 elmapfn 
 |-  ( g e. ( ~P B ^m ~P B ) -> g Fn ~P B )
122 121 ad2antrl 
 |-  ( ( ph /\ ( g e. ( ~P B ^m ~P B ) /\ f = ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) ) -> g Fn ~P B )
123 difeq2 
 |-  ( t = s -> ( B \ t ) = ( B \ s ) )
124 123 fveq2d 
 |-  ( t = s -> ( f ` ( B \ t ) ) = ( f ` ( B \ s ) ) )
125 124 difeq2d 
 |-  ( t = s -> ( B \ ( f ` ( B \ t ) ) ) = ( B \ ( f ` ( B \ s ) ) ) )
126 3 difexd 
 |-  ( ph -> ( B \ ( f ` ( B \ t ) ) ) e. _V )
127 126 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 )
128 3 difexd 
 |-  ( ph -> ( B \ ( f ` ( B \ s ) ) ) e. _V )
129 128 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 )
130 122 125 127 129 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 ) ) ) ) )
131 120 130 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 ) ) ) ) )
132 92 131 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 ) ) ) ) ) )
133 74 132 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 ) ) ) ) ) ) )
134 133 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 ) ) ) ) ) )
135 1 2 3 dssmapfvd 
 |-  ( ph -> D = ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )
136 135 cnveqd 
 |-  ( ph -> `' D = `' ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )
137 fveq1 
 |-  ( f = g -> ( f ` ( b \ s ) ) = ( g ` ( b \ s ) ) )
138 137 difeq2d 
 |-  ( f = g -> ( b \ ( f ` ( b \ s ) ) ) = ( b \ ( g ` ( b \ s ) ) ) )
139 138 mpteq2dv 
 |-  ( f = g -> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) = ( s e. ~P b |-> ( b \ ( g ` ( b \ s ) ) ) ) )
140 difeq2 
 |-  ( s = z -> ( b \ s ) = ( b \ z ) )
141 140 fveq2d 
 |-  ( s = z -> ( g ` ( b \ s ) ) = ( g ` ( b \ z ) ) )
142 141 difeq2d 
 |-  ( s = z -> ( b \ ( g ` ( b \ s ) ) ) = ( b \ ( g ` ( b \ z ) ) ) )
143 142 cbvmptv 
 |-  ( s e. ~P b |-> ( b \ ( g ` ( b \ s ) ) ) ) = ( z e. ~P b |-> ( b \ ( g ` ( b \ z ) ) ) )
144 139 143 eqtrdi 
 |-  ( f = g -> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) = ( z e. ~P b |-> ( b \ ( g ` ( b \ z ) ) ) ) )
145 144 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 ) ) ) ) )
146 145 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 ) ) ) ) ) )
147 1 146 eqtri 
 |-  O = ( b e. _V |-> ( g e. ( ~P b ^m ~P b ) |-> ( z e. ~P b |-> ( b \ ( g ` ( b \ z ) ) ) ) ) )
148 147 2 3 dssmapfvd 
 |-  ( ph -> D = ( g e. ( ~P B ^m ~P B ) |-> ( z e. ~P B |-> ( B \ ( g ` ( B \ z ) ) ) ) ) )
149 134 136 148 3eqtr4d 
 |-  ( ph -> `' D = D )