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

Metamath Proof Explorer

Theorem mapfien2

Description: Equinumerousity relation for sets of finitely supported functions. (Contributed by Stefan O'Rear, 9-Jul-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Hypotheses mapfien2.s 
|- S = { x e. ( B ^m A ) | x finSupp .0. }
mapfien2.t 
|- T = { x e. ( D ^m C ) | x finSupp W }
mapfien2.ac 
|- ( ph -> A ~~ C )
mapfien2.bd 
|- ( ph -> B ~~ D )
mapfien2.z 
|- ( ph -> .0. e. B )
mapfien2.w 
|- ( ph -> W e. D )
Assertion mapfien2 
|- ( ph -> S ~~ T )

Proof

Step Hyp Ref Expression
1 mapfien2.s 
 |-  S = { x e. ( B ^m A ) | x finSupp .0. }
2 mapfien2.t 
 |-  T = { x e. ( D ^m C ) | x finSupp W }
3 mapfien2.ac 
 |-  ( ph -> A ~~ C )
4 mapfien2.bd 
 |-  ( ph -> B ~~ D )
5 mapfien2.z 
 |-  ( ph -> .0. e. B )
6 mapfien2.w 
 |-  ( ph -> W e. D )
7 enfixsn 
 |-  ( ( .0. e. B /\ W e. D /\ B ~~ D ) -> E. y ( y : B -1-1-onto-> D /\ ( y ` .0. ) = W ) )
8 5 6 4 7 syl3anc 
 |-  ( ph -> E. y ( y : B -1-1-onto-> D /\ ( y ` .0. ) = W ) )
9 bren 
 |-  ( A ~~ C <-> E. z z : A -1-1-onto-> C )
10 3 9 sylib 
 |-  ( ph -> E. z z : A -1-1-onto-> C )
11 eqid 
 |-  { x e. ( D ^m C ) | x finSupp ( y ` .0. ) } = { x e. ( D ^m C ) | x finSupp ( y ` .0. ) }
12 eqid 
 |-  ( y ` .0. ) = ( y ` .0. )
13 f1ocnv 
 |-  ( z : A -1-1-onto-> C -> `' z : C -1-1-onto-> A )
14 13 3ad2ant2 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> `' z : C -1-1-onto-> A )
15 simp3 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> y : B -1-1-onto-> D )
16 3 3ad2ant1 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> A ~~ C )
17 relen 
 |-  Rel ~~
18 17 brrelex1i 
 |-  ( A ~~ C -> A e. _V )
19 16 18 syl 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> A e. _V )
20 4 3ad2ant1 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> B ~~ D )
21 17 brrelex1i 
 |-  ( B ~~ D -> B e. _V )
22 20 21 syl 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> B e. _V )
23 17 brrelex2i 
 |-  ( A ~~ C -> C e. _V )
24 16 23 syl 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> C e. _V )
25 17 brrelex2i 
 |-  ( B ~~ D -> D e. _V )
26 20 25 syl 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> D e. _V )
27 5 3ad2ant1 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> .0. e. B )
28 1 11 12 14 15 19 22 24 26 27 mapfien 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> ( w e. S |-> ( y o. ( w o. `' z ) ) ) : S -1-1-onto-> { x e. ( D ^m C ) | x finSupp ( y ` .0. ) } )
29 ovex 
 |-  ( B ^m A ) e. _V
30 1 29 rabex2 
 |-  S e. _V
31 30 f1oen 
 |-  ( ( w e. S |-> ( y o. ( w o. `' z ) ) ) : S -1-1-onto-> { x e. ( D ^m C ) | x finSupp ( y ` .0. ) } -> S ~~ { x e. ( D ^m C ) | x finSupp ( y ` .0. ) } )
32 28 31 syl 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) -> S ~~ { x e. ( D ^m C ) | x finSupp ( y ` .0. ) } )
33 32 3adant3r 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ ( y : B -1-1-onto-> D /\ ( y ` .0. ) = W ) ) -> S ~~ { x e. ( D ^m C ) | x finSupp ( y ` .0. ) } )
34 breq2 
 |-  ( ( y ` .0. ) = W -> ( x finSupp ( y ` .0. ) <-> x finSupp W ) )
35 34 rabbidv 
 |-  ( ( y ` .0. ) = W -> { x e. ( D ^m C ) | x finSupp ( y ` .0. ) } = { x e. ( D ^m C ) | x finSupp W } )
36 35 2 eqtr4di 
 |-  ( ( y ` .0. ) = W -> { x e. ( D ^m C ) | x finSupp ( y ` .0. ) } = T )
37 36 adantl 
 |-  ( ( y : B -1-1-onto-> D /\ ( y ` .0. ) = W ) -> { x e. ( D ^m C ) | x finSupp ( y ` .0. ) } = T )
38 37 3ad2ant3 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ ( y : B -1-1-onto-> D /\ ( y ` .0. ) = W ) ) -> { x e. ( D ^m C ) | x finSupp ( y ` .0. ) } = T )
39 33 38 breqtrd 
 |-  ( ( ph /\ z : A -1-1-onto-> C /\ ( y : B -1-1-onto-> D /\ ( y ` .0. ) = W ) ) -> S ~~ T )
40 39 3exp 
 |-  ( ph -> ( z : A -1-1-onto-> C -> ( ( y : B -1-1-onto-> D /\ ( y ` .0. ) = W ) -> S ~~ T ) ) )
41 40 exlimdv 
 |-  ( ph -> ( E. z z : A -1-1-onto-> C -> ( ( y : B -1-1-onto-> D /\ ( y ` .0. ) = W ) -> S ~~ T ) ) )
42 10 41 mpd 
 |-  ( ph -> ( ( y : B -1-1-onto-> D /\ ( y ` .0. ) = W ) -> S ~~ T ) )
43 42 exlimdv 
 |-  ( ph -> ( E. y ( y : B -1-1-onto-> D /\ ( y ` .0. ) = W ) -> S ~~ T ) )
44 8 43 mpd 
 |-  ( ph -> S ~~ T )