Theorem enrelmapr

Description: The set of all possible relations between two sets is equinumerous to the set of all mappings from one set to the powerset of the other. (Contributed by RP, 27-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		xpcomeng	|- ( ( A e. V /\ B e. W ) -> ( A X. B ) ~~ ( B X. A ) )
2		pwen	|- ( ( A X. B ) ~~ ( B X. A ) -> ~P ( A X. B ) ~~ ~P ( B X. A ) )
3	1 2	syl	|- ( ( A e. V /\ B e. W ) -> ~P ( A X. B ) ~~ ~P ( B X. A ) )
4		enrelmap	|- ( ( B e. W /\ A e. V ) -> ~P ( B X. A ) ~~ ( ~P A ^m B ) )
5	4	ancoms	|- ( ( A e. V /\ B e. W ) -> ~P ( B X. A ) ~~ ( ~P A ^m B ) )
6		entr	|- ( ( ~P ( A X. B ) ~~ ~P ( B X. A ) /\ ~P ( B X. A ) ~~ ( ~P A ^m B ) ) -> ~P ( A X. B ) ~~ ( ~P A ^m B ) )
7	3 5 6	syl2anc	|- ( ( A e. V /\ B e. W ) -> ~P ( A X. B ) ~~ ( ~P A ^m B ) )