Metamath Proof Explorer


Theorem fsovf1od

Description: The value of ( A O B ) is a bijection, 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. (Contributed by RP, 27-Apr-2021)

Ref Expression
Hypotheses fsovd.fs 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏m 𝑎 ) ↦ ( 𝑦𝑏 ↦ { 𝑥𝑎𝑦 ∈ ( 𝑓𝑥 ) } ) ) )
fsovd.a ( 𝜑𝐴𝑉 )
fsovd.b ( 𝜑𝐵𝑊 )
fsovfvd.g 𝐺 = ( 𝐴 𝑂 𝐵 )
Assertion fsovf1od ( 𝜑𝐺 : ( 𝒫 𝐵m 𝐴 ) –1-1-onto→ ( 𝒫 𝐴m 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fsovd.fs 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏m 𝑎 ) ↦ ( 𝑦𝑏 ↦ { 𝑥𝑎𝑦 ∈ ( 𝑓𝑥 ) } ) ) )
2 fsovd.a ( 𝜑𝐴𝑉 )
3 fsovd.b ( 𝜑𝐵𝑊 )
4 fsovfvd.g 𝐺 = ( 𝐴 𝑂 𝐵 )
5 1 2 3 4 fsovfd ( 𝜑𝐺 : ( 𝒫 𝐵m 𝐴 ) ⟶ ( 𝒫 𝐴m 𝐵 ) )
6 5 ffnd ( 𝜑𝐺 Fn ( 𝒫 𝐵m 𝐴 ) )
7 eqid ( 𝐵 𝑂 𝐴 ) = ( 𝐵 𝑂 𝐴 )
8 1 3 2 7 fsovfd ( 𝜑 → ( 𝐵 𝑂 𝐴 ) : ( 𝒫 𝐴m 𝐵 ) ⟶ ( 𝒫 𝐵m 𝐴 ) )
9 8 ffnd ( 𝜑 → ( 𝐵 𝑂 𝐴 ) Fn ( 𝒫 𝐴m 𝐵 ) )
10 1 2 3 4 7 fsovcnvd ( 𝜑 𝐺 = ( 𝐵 𝑂 𝐴 ) )
11 10 fneq1d ( 𝜑 → ( 𝐺 Fn ( 𝒫 𝐴m 𝐵 ) ↔ ( 𝐵 𝑂 𝐴 ) Fn ( 𝒫 𝐴m 𝐵 ) ) )
12 9 11 mpbird ( 𝜑 𝐺 Fn ( 𝒫 𝐴m 𝐵 ) )
13 dff1o4 ( 𝐺 : ( 𝒫 𝐵m 𝐴 ) –1-1-onto→ ( 𝒫 𝐴m 𝐵 ) ↔ ( 𝐺 Fn ( 𝒫 𝐵m 𝐴 ) ∧ 𝐺 Fn ( 𝒫 𝐴m 𝐵 ) ) )
14 6 12 13 sylanbrc ( 𝜑𝐺 : ( 𝒫 𝐵m 𝐴 ) –1-1-onto→ ( 𝒫 𝐴m 𝐵 ) )