Metamath Proof Explorer


Theorem enmappw

Description: The set of all mappings from one set to the powerset of the other is equinumerous to the set of all mappings from the second set to the powerset of the first. (Contributed by RP, 27-Apr-2021)

Ref Expression
Assertion enmappw
|- ( ( A e. V /\ B e. W ) -> ( ~P B ^m A ) ~~ ( ~P A ^m B ) )

Proof

Step Hyp Ref Expression
1 enrelmap
 |-  ( ( A e. V /\ B e. W ) -> ~P ( A X. B ) ~~ ( ~P B ^m A ) )
2 1 ensymd
 |-  ( ( A e. V /\ B e. W ) -> ( ~P B ^m A ) ~~ ~P ( A X. B ) )
3 enrelmapr
 |-  ( ( A e. V /\ B e. W ) -> ~P ( A X. B ) ~~ ( ~P A ^m B ) )
4 entr
 |-  ( ( ( ~P B ^m A ) ~~ ~P ( A X. B ) /\ ~P ( A X. B ) ~~ ( ~P A ^m B ) ) -> ( ~P B ^m A ) ~~ ( ~P A ^m B ) )
5 2 3 4 syl2anc
 |-  ( ( A e. V /\ B e. W ) -> ( ~P B ^m A ) ~~ ( ~P A ^m B ) )