Step |
Hyp |
Ref |
Expression |
1 |
|
funmpt |
⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
2 |
|
ctex |
⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V ) |
3 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
4 |
3
|
dmmptss |
⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 |
5 |
|
ssdomg |
⊢ ( 𝐴 ∈ V → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ 𝐴 ) ) |
6 |
2 4 5
|
mpisyl |
⊢ ( 𝐴 ≼ ω → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ 𝐴 ) |
7 |
|
domtr |
⊢ ( ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ 𝐴 ∧ 𝐴 ≼ ω ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) |
8 |
6 7
|
mpancom |
⊢ ( 𝐴 ≼ ω → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) |
9 |
|
funfn |
⊢ ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) |
10 |
|
fnct |
⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) |
11 |
9 10
|
sylanb |
⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) |
12 |
1 8 11
|
sylancr |
⊢ ( 𝐴 ≼ ω → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) |