Theorem rfovf1od

Description: The value of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B , is a bijection. (Contributed by RP, 27-Apr-2021)

	Ref	Expression
Hypotheses	rfovd.rf	|- O = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( x e. a |-> { y e. b | x r y } ) ) )
	rfovd.a	|- ( ph -> A e. V )
	rfovd.b	|- ( ph -> B e. W )
	rfovcnvf1od.f	|- F = ( A O B )
Assertion	rfovf1od	|- ( ph -> F : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) )

Proof

Step	Hyp	Ref	Expression
1		rfovd.rf	|- O = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( x e. a |-> { y e. b | x r y } ) ) )
2		rfovd.a	|- ( ph -> A e. V )
3		rfovd.b	|- ( ph -> B e. W )
4		rfovcnvf1od.f	|- F = ( A O B )
5	1 2 3 4	rfovcnvf1od	|- ( ph -> ( F : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) /\ `' F = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) )
6	5	simpld	|- ( ph -> F : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) )