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 𝐵 ) ) |