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 2 pwex 
 |-  ~P B e. _V
8 7 1 elmap 
 |-  ( f e. ( ~P B ^m A ) <-> f : A --> ~P B )
9 8 birani 
 |-  ( ( f e. ( ~P B ^m A ) /\ r = { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) -> f : A --> ~P B )
10 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 ) ) } )
11 1 2 9 10 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 ) ) )
12 11 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 ) ) )
13 3 6 12 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 } )
14 13 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 }
15 1 7 maprnin 
 |-  ( ( ~P B i^i Fin ) ^m A ) = { f e. ( ~P B ^m A ) | ran f C_ Fin }
16 nfcv 
 |-  F/_ f ( ( ~P B i^i Fin ) ^m A )
17 nfrab1 
 |-  F/_ f { f e. ( ~P B ^m A ) | ran f C_ Fin }
18 16 17 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 } )
19 15 18 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 }
20 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 ) }
21 4 19 20 3eqtri 
 |-  S = { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) }
22 dfin5 
 |-  ( ~P ( A X. B ) i^i Fin ) = { r e. ~P ( A X. B ) | r e. Fin }
23 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 } ) )
24 21 22 23 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 } )
25 21 reseq2i 
 |-  ( M |` S ) = ( M |` { f e. ( ~P B ^m A ) | ( ran f C_ Fin /\ ( f supp (/) ) e. Fin ) } )
26 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 } ) )
27 25 26 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 } )
28 24 27 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 ) )
29 14 28 mpbi 
 |-  ( M |` S ) : S -1-1-onto-> ( ~P ( A X. B ) i^i Fin )