Metamath Proof Explorer


Theorem rfovcnvd

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

Ref Expression
Hypotheses rfovd.rf 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥𝑎 ↦ { 𝑦𝑏𝑥 𝑟 𝑦 } ) ) )
rfovd.a ( 𝜑𝐴𝑉 )
rfovd.b ( 𝜑𝐵𝑊 )
rfovcnvf1od.f 𝐹 = ( 𝐴 𝑂 𝐵 )
Assertion rfovcnvd ( 𝜑 𝐹 = ( 𝑓 ∈ ( 𝒫 𝐵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 simprd ( 𝜑 𝐹 = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) ) } ) )