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 𝐴 ) ↦ ( 𝑦 ∈ 𝐵 ↦ { 𝑥 ∈ 𝐴 ∣ 𝑦 ∈ ( 𝑓 ‘ 𝑥 ) } ) ) ) |