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	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) ) )
	rfovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	rfovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	rfovcnvf1od.f	⊢ 𝐹 = ( 𝐴 𝑂 𝐵 )
Assertion	rfovf1od	⊢ ( 𝜑 → 𝐹 : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rfovd.rf	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) ) )
2		rfovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		rfovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		rfovcnvf1od.f	⊢ 𝐹 = ( 𝐴 𝑂 𝐵 )
5	1 2 3 4	rfovcnvf1od	⊢ ( 𝜑 → ( 𝐹 : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝐴 ) ∧ ◡ 𝐹 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) ) } ) ) )
6	5	simpld	⊢ ( 𝜑 → 𝐹 : 𝒫 ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝐴 ) )