Metamath Proof Explorer

Theorem fpwrelmapffs

Description: Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses fpwrelmap.1 
|- A e. _V
fpwrelmap.2 
|- B e. _V
fpwrelmap.3 
|- M = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } )
fpwrelmapffs.1 
|- S = { f e. ( ( ~P B i^i Fin ) ^m A ) | ( f supp (/) ) e. Fin }
Assertion fpwrelmapffs 
|- ( M |` S ) : S -1-1-onto-> ( ~P ( A X. B ) i^i Fin )

Proof

Step Hyp Ref Expression
1 fpwrelmap.1 
 |-  A e. _V
2 fpwrelmap.2 
 |-  B e. _V
3 fpwrelmap.3 
 |-  M = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } )
4 fpwrelmapffs.1 
 |-  S = { f e. ( ( ~P B i^i Fin ) ^m A ) | ( f supp (/) ) e. Fin }
5 1 2 3 fpwrelmap 
 |-  M : ( ~P B ^m A ) -1-1-onto-> ~P ( A X. B )
6 5 a1i 
 |-  ( T. -> M : ( ~P B ^m A ) -1-1-onto-> ~P ( A X. B ) )
7 simpl 
 |-  ( ( f e. ( ~P B ^m A ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> f e. ( ~P B ^m A ) )
8 2 pwex 
 |-  ~P B e. _V
9 8 1 elmap 
 |-  ( f e. ( ~P B ^m A ) <-> f : A --> ~P B )
10 7 9 sylib 
 |-  ( ( f e. ( ~P B ^m A ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> f : A --> ~P B )
11 simpr 
 |-  ( ( f e. ( ~P B ^m A ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } )
12 1 2 10 11 fpwrelmapffslem 
 |-  ( ( f e. ( ~P B ^m A ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> ( r e. Fin <-> ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) ) )
13 12 3adant1 
 |-  ( ( T. /\ f e. ( ~P B ^m A ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> ( r e. Fin <-> ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) ) )
14 3 6 13 f1oresrab 
 |-  ( T. -> ( M |` { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } ) : { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } -1-1-onto-> { r e. ~P ( A X. B ) | r e. Fin } )
15 14 mptru 
 |-  ( M |` { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } ) : { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } -1-1-onto-> { r e. ~P ( A X. B ) | r e. Fin }
16 1 8 maprnin 
 |-  ( ( ~P B i^i Fin ) ^m A ) = { f e. ( ~P B ^m A ) | ran f C_ Fin }
17 nfcv 
 |-  F/_ f ( ( ~P B i^i Fin ) ^m A )
18 nfrab1 
 |-  F/_ f { f e. ( ~P B ^m A ) | ran f C_ Fin }
19 17 18 rabeqf 
 |-  ( ( ( ~P B i^i Fin ) ^m A ) = { f e. ( ~P B ^m A ) | ran f C_ Fin } -> { f e. ( ( ~P B i^i Fin ) ^m A ) | ( f supp (/) ) e. Fin } = { f e. { f e. ( ~P B ^m A ) | ran f C_ Fin } | ( f supp (/) ) e. Fin } )
20 16 19 ax-mp 
 |-  { f e. ( ( ~P B i^i Fin ) ^m A ) | ( f supp (/) ) e. Fin } = { f e. { f e. ( ~P B ^m A ) | ran f C_ Fin } | ( f supp (/) ) e. Fin }
21 rabrab 
 |-  { f e. { f e. ( ~P B ^m A ) | ran f C_ Fin } | ( f supp (/) ) e. Fin } = { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) }
22 4 20 21 3eqtri 
 |-  S = { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) }
23 dfin5 
 |-  ( ~P ( A X. B ) i^i Fin ) = { r e. ~P ( A X. B ) | r e. Fin }
24 f1oeq23 
 |-  ( ( S = { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } /\ ( ~P ( A X. B ) i^i Fin ) = { r e. ~P ( A X. B ) | r e. Fin } ) -> ( ( M |` S ) : S -1-1-onto-> ( ~P ( A X. B ) i^i Fin ) <-> ( M |` S ) : { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } -1-1-onto-> { r e. ~P ( A X. B ) | r e. Fin } ) )
25 22 23 24 mp2an 
 |-  ( ( M |` S ) : S -1-1-onto-> ( ~P ( A X. B ) i^i Fin ) <-> ( M |` S ) : { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } -1-1-onto-> { r e. ~P ( A X. B ) | r e. Fin } )
26 22 reseq2i 
 |-  ( M |` S ) = ( M |` { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } )
27 f1oeq1 
 |-  ( ( M |` S ) = ( M |` { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } ) -> ( ( M |` S ) : { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } -1-1-onto-> { r e. ~P ( A X. B ) | r e. Fin } <-> ( M |` { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } ) : { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } -1-1-onto-> { r e. ~P ( A X. B ) | r e. Fin } ) )
28 26 27 ax-mp 
 |-  ( ( M |` S ) : { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } -1-1-onto-> { r e. ~P ( A X. B ) | r e. Fin } <-> ( M |` { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } ) : { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } -1-1-onto-> { r e. ~P ( A X. B ) | r e. Fin } )
29 25 28 bitr2i 
 |-  ( ( M |` { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } ) : { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } -1-1-onto-> { r e. ~P ( A X. B ) | r e. Fin } <-> ( M |` S ) : S -1-1-onto-> ( ~P ( A X. B ) i^i Fin ) )
30 15 29 mpbi 
 |-  ( M |` S ) : S -1-1-onto-> ( ~P ( A X. B ) i^i Fin )