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 ) ) |
| 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 ) ) |