Description: The value of the converse of ( A O B ) , 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, evaluated at function F . (Contributed by RP, 27-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fsovd.fs | ⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) | |
| fsovd.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | ||
| fsovd.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) | ||
| fsovfvd.g | ⊢ 𝐺 = ( 𝐴 𝑂 𝐵 ) | ||
| fsovcnvfvd.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝒫 𝐴 ↑m 𝐵 ) ) | ||
| Assertion | fsovcnvfvd | ⊢ ( 𝜑 → ( ◡ 𝐺 ‘ 𝐹 ) = ( 𝑦 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fsovd.fs | ⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑦 ∈ 𝑏 ↦ { 𝑥 ∈ 𝑎 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) | |
| 2 | fsovd.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
| 3 | fsovd.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) | |
| 4 | fsovfvd.g | ⊢ 𝐺 = ( 𝐴 𝑂 𝐵 ) | |
| 5 | fsovcnvfvd.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝒫 𝐴 ↑m 𝐵 ) ) | |
| 6 | eqid | ⊢ ( 𝐵 𝑂 𝐴 ) = ( 𝐵 𝑂 𝐴 ) | |
| 7 | 1 2 3 4 6 | fsovcnvd | ⊢ ( 𝜑 → ◡ 𝐺 = ( 𝐵 𝑂 𝐴 ) ) |
| 8 | 7 | fveq1d | ⊢ ( 𝜑 → ( ◡ 𝐺 ‘ 𝐹 ) = ( ( 𝐵 𝑂 𝐴 ) ‘ 𝐹 ) ) |
| 9 | 1 3 2 6 5 | fsovfvd | ⊢ ( 𝜑 → ( ( 𝐵 𝑂 𝐴 ) ‘ 𝐹 ) = ( 𝑦 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ) ) |
| 10 | 8 9 | eqtrd | ⊢ ( 𝜑 → ( ◡ 𝐺 ‘ 𝐹 ) = ( 𝑦 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } ) ) |