Step |
Hyp |
Ref |
Expression |
1 |
|
mptexgf.a |
⊢ Ⅎ 𝑥 𝐴 |
2 |
|
funmpt |
⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
3 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
4 |
3
|
dmmpt |
⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } |
5 |
|
tru |
⊢ ⊤ |
6 |
5
|
2a1i |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝐵 ∈ V → ⊤ ) ) |
7 |
6
|
ss2rabi |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ⊆ { 𝑥 ∈ 𝐴 ∣ ⊤ } |
8 |
1
|
rabtru |
⊢ { 𝑥 ∈ 𝐴 ∣ ⊤ } = 𝐴 |
9 |
7 8
|
sseqtri |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ⊆ 𝐴 |
10 |
4 9
|
eqsstri |
⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 |
11 |
|
ssexg |
⊢ ( ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) |
12 |
10 11
|
mpan |
⊢ ( 𝐴 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) |
13 |
|
funex |
⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) |
14 |
2 12 13
|
sylancr |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) |