Step |
Hyp |
Ref |
Expression |
1 |
|
1arympt1.f |
⊢ 𝐹 = ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) ↦ ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) ) |
2 |
|
eqid |
⊢ ( 𝑋 ↑m { 0 } ) = ( 𝑋 ↑m { 0 } ) |
3 |
|
id |
⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) → 𝑥 ∈ ( 𝑋 ↑m { 0 } ) ) |
4 |
|
c0ex |
⊢ 0 ∈ V |
5 |
4
|
snid |
⊢ 0 ∈ { 0 } |
6 |
5
|
a1i |
⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) → 0 ∈ { 0 } ) |
7 |
2 3 6
|
mapfvd |
⊢ ( 𝑥 ∈ ( 𝑋 ↑m { 0 } ) → ( 𝑥 ‘ 0 ) ∈ 𝑋 ) |
8 |
|
ffvelrn |
⊢ ( ( 𝐴 : 𝑋 ⟶ 𝑋 ∧ ( 𝑥 ‘ 0 ) ∈ 𝑋 ) → ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) ∈ 𝑋 ) |
9 |
7 8
|
sylan2 |
⊢ ( ( 𝐴 : 𝑋 ⟶ 𝑋 ∧ 𝑥 ∈ ( 𝑋 ↑m { 0 } ) ) → ( 𝐴 ‘ ( 𝑥 ‘ 0 ) ) ∈ 𝑋 ) |
10 |
9 1
|
fmptd |
⊢ ( 𝐴 : 𝑋 ⟶ 𝑋 → 𝐹 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) |
11 |
|
1aryfvalel |
⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 ∈ ( 1 -aryF 𝑋 ) ↔ 𝐹 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ) |
12 |
10 11
|
syl5ibr |
⊢ ( 𝑋 ∈ 𝑉 → ( 𝐴 : 𝑋 ⟶ 𝑋 → 𝐹 ∈ ( 1 -aryF 𝑋 ) ) ) |
13 |
12
|
imp |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 : 𝑋 ⟶ 𝑋 ) → 𝐹 ∈ ( 1 -aryF 𝑋 ) ) |