Description: If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (Contributed by Mario Carneiro, 15-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | f1imaeng | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1ores | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) | |
2 | f1oeng | ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) ) | |
3 | 2 | ancoms | ⊢ ( ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) ) |
4 | 1 3 | stoic3 | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) ) |
5 | 4 | ensymd | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 ) |