Metamath Proof Explorer


Theorem fsovd

Description: Value of the operator, ( A O B ) , 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, A and B . (Contributed by RP, 25-Apr-2021)

Ref Expression
Hypotheses fsovd.fs 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏m 𝑎 ) ↦ ( 𝑦𝑏 ↦ { 𝑥𝑎𝑦 ∈ ( 𝑓𝑥 ) } ) ) )
fsovd.a ( 𝜑𝐴𝑉 )
fsovd.b ( 𝜑𝐵𝑊 )
Assertion fsovd ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ ( 𝑦𝐵 ↦ { 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) } ) ) )

Proof

Step Hyp Ref Expression
1 fsovd.fs 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏m 𝑎 ) ↦ ( 𝑦𝑏 ↦ { 𝑥𝑎𝑦 ∈ ( 𝑓𝑥 ) } ) ) )
2 fsovd.a ( 𝜑𝐴𝑉 )
3 fsovd.b ( 𝜑𝐵𝑊 )
4 1 a1i ( 𝜑𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏m 𝑎 ) ↦ ( 𝑦𝑏 ↦ { 𝑥𝑎𝑦 ∈ ( 𝑓𝑥 ) } ) ) ) )
5 pweq ( 𝑏 = 𝐵 → 𝒫 𝑏 = 𝒫 𝐵 )
6 5 adantl ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → 𝒫 𝑏 = 𝒫 𝐵 )
7 simpl ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → 𝑎 = 𝐴 )
8 6 7 oveq12d ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( 𝒫 𝑏m 𝑎 ) = ( 𝒫 𝐵m 𝐴 ) )
9 simpr ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
10 rabeq ( 𝑎 = 𝐴 → { 𝑥𝑎𝑦 ∈ ( 𝑓𝑥 ) } = { 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) } )
11 10 adantr ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → { 𝑥𝑎𝑦 ∈ ( 𝑓𝑥 ) } = { 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) } )
12 9 11 mpteq12dv ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( 𝑦𝑏 ↦ { 𝑥𝑎𝑦 ∈ ( 𝑓𝑥 ) } ) = ( 𝑦𝐵 ↦ { 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) } ) )
13 8 12 mpteq12dv ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( 𝑓 ∈ ( 𝒫 𝑏m 𝑎 ) ↦ ( 𝑦𝑏 ↦ { 𝑥𝑎𝑦 ∈ ( 𝑓𝑥 ) } ) ) = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ ( 𝑦𝐵 ↦ { 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) } ) ) )
14 13 adantl ( ( 𝜑 ∧ ( 𝑎 = 𝐴𝑏 = 𝐵 ) ) → ( 𝑓 ∈ ( 𝒫 𝑏m 𝑎 ) ↦ ( 𝑦𝑏 ↦ { 𝑥𝑎𝑦 ∈ ( 𝑓𝑥 ) } ) ) = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ ( 𝑦𝐵 ↦ { 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) } ) ) )
15 2 elexd ( 𝜑𝐴 ∈ V )
16 3 elexd ( 𝜑𝐵 ∈ V )
17 ovex ( 𝒫 𝐵m 𝐴 ) ∈ V
18 17 mptex ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ ( 𝑦𝐵 ↦ { 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) } ) ) ∈ V
19 18 a1i ( 𝜑 → ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ ( 𝑦𝐵 ↦ { 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) } ) ) ∈ V )
20 4 14 15 16 19 ovmpod ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( 𝑓 ∈ ( 𝒫 𝐵m 𝐴 ) ↦ ( 𝑦𝐵 ↦ { 𝑥𝐴𝑦 ∈ ( 𝑓𝑥 ) } ) ) )