Theorem fsovcnvd

Description: The value of the converse ( A O B ) is ( B O A ) , where O is the operator which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, gives a family of functions that include their own inverse. (Contributed by RP, 27-Apr-2021)

	Ref	Expression
Hypotheses	fsovd.fs	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
	fsovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	fsovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	fsovfvd.g	⊢ 𝐺 = ( 𝐴 𝑂 𝐵 )
	fsovcnvlem.h	⊢ 𝐻 = ( 𝐵 𝑂 𝐴 )
Assertion	fsovcnvd	⊢ ( 𝜑 → ◡ 𝐺 = 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		fsovd.fs	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) )
2		fsovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		fsovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		fsovfvd.g	⊢ 𝐺 = ( 𝐴 𝑂 𝐵 )
5		fsovcnvlem.h	⊢ 𝐻 = ( 𝐵 𝑂 𝐴 )
6	1 2 3 4	fsovfd	⊢ ( 𝜑 → 𝐺 : ( 𝒫 𝐵 ↑m 𝐴 ) ⟶ ( 𝒫 𝐴 ↑m 𝐵 ) )
7	1 3 2 5	fsovfd	⊢ ( 𝜑 → 𝐻 : ( 𝒫 𝐴 ↑m 𝐵 ) ⟶ ( 𝒫 𝐵 ↑m 𝐴 ) )
8	1 2 3 4 5	fsovcnvlem	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐺 ) = ( I ↾ ( 𝒫 𝐵 ↑m 𝐴 ) ) )
9	1 3 2 5 4	fsovcnvlem	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐻 ) = ( I ↾ ( 𝒫 𝐴 ↑m 𝐵 ) ) )
10	6 7 8 9	2fcoidinvd	⊢ ( 𝜑 → ◡ 𝐺 = 𝐻 )