Step |
Hyp |
Ref |
Expression |
1 |
|
elmapi |
⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → 𝐴 : ( 𝐼 × 𝐽 ) ⟶ 𝐵 ) |
2 |
|
tposf |
⊢ ( 𝐴 : ( 𝐼 × 𝐽 ) ⟶ 𝐵 → tpos 𝐴 : ( 𝐽 × 𝐼 ) ⟶ 𝐵 ) |
3 |
1 2
|
syl |
⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → tpos 𝐴 : ( 𝐽 × 𝐼 ) ⟶ 𝐵 ) |
4 |
|
elmapex |
⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → ( 𝐵 ∈ V ∧ ( 𝐼 × 𝐽 ) ∈ V ) ) |
5 |
|
cnvxp |
⊢ ◡ ( 𝐼 × 𝐽 ) = ( 𝐽 × 𝐼 ) |
6 |
|
cnvexg |
⊢ ( ( 𝐼 × 𝐽 ) ∈ V → ◡ ( 𝐼 × 𝐽 ) ∈ V ) |
7 |
5 6
|
eqeltrrid |
⊢ ( ( 𝐼 × 𝐽 ) ∈ V → ( 𝐽 × 𝐼 ) ∈ V ) |
8 |
7
|
anim2i |
⊢ ( ( 𝐵 ∈ V ∧ ( 𝐼 × 𝐽 ) ∈ V ) → ( 𝐵 ∈ V ∧ ( 𝐽 × 𝐼 ) ∈ V ) ) |
9 |
|
elmapg |
⊢ ( ( 𝐵 ∈ V ∧ ( 𝐽 × 𝐼 ) ∈ V ) → ( tpos 𝐴 ∈ ( 𝐵 ↑m ( 𝐽 × 𝐼 ) ) ↔ tpos 𝐴 : ( 𝐽 × 𝐼 ) ⟶ 𝐵 ) ) |
10 |
4 8 9
|
3syl |
⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → ( tpos 𝐴 ∈ ( 𝐵 ↑m ( 𝐽 × 𝐼 ) ) ↔ tpos 𝐴 : ( 𝐽 × 𝐼 ) ⟶ 𝐵 ) ) |
11 |
3 10
|
mpbird |
⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → tpos 𝐴 ∈ ( 𝐵 ↑m ( 𝐽 × 𝐼 ) ) ) |