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=\left(a\in \mathrm{V},b\in \mathrm{V}⟼\left(r\in 𝒫\left(a\times b\right)⟼\left(x\in a⟼\left\{y\in b|xry\right\}\right)\right)\right)$$
	rfovd.a	$$⊢\phi \to A\in V$$
	rfovd.b	$$⊢\phi \to B\in W$$
	rfovcnvf1od.f	$$⊢F=AOB$$
Assertion	rfovf1od	$$⊢\phi \to F:𝒫\left(A\times B\right)\underset{1-1\; onto}{⟶}{𝒫B}^A$$

Proof

Step	Hyp	Ref	Expression
1		rfovd.rf	$$⊢O=\left(a\in \mathrm{V},b\in \mathrm{V}⟼\left(r\in 𝒫\left(a\times b\right)⟼\left(x\in a⟼\left\{y\in b|xry\right\}\right)\right)\right)$$
2		rfovd.a	$$⊢\phi \to A\in V$$
3		rfovd.b	$$⊢\phi \to B\in W$$
4		rfovcnvf1od.f	$$⊢F=AOB$$
5	1 2 3 4	rfovcnvf1od	$$⊢\phi \to \left(F:𝒫\left(A\times B\right)\underset{1-1\; onto}{⟶}{𝒫B}^A\wedge F^{-1}=\left(f\in \left({𝒫B}^A\right)⟼\left\{⟨x,y⟩|\left(x\in A\wedge y\in f\left(x\right)\right)\right\}\right)\right)$$
6	5	simpld	$$⊢\phi \to F:𝒫\left(A\times B\right)\underset{1-1\; onto}{⟶}{𝒫B}^A$$