Description: An image set of a countable set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mptctf.1 | ⊢ Ⅎ 𝑥 𝐴 | |
| Assertion | abrexctf | ⊢ ( 𝐴 ≼ ω → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≼ ω ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mptctf.1 | ⊢ Ⅎ 𝑥 𝐴 | |
| 2 | eqid | ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |
| 3 | 2 | rnmpt | ⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } |
| 4 | 1 | mptctf | ⊢ ( 𝐴 ≼ ω → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) |
| 5 | rnct | ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) | |
| 6 | 4 5 | syl | ⊢ ( 𝐴 ≼ ω → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) |
| 7 | 3 6 | eqbrtrrid | ⊢ ( 𝐴 ≼ ω → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≼ ω ) |