Description: If a set function is one-to-one, then a subset of its domain is equinumerous to the image of that subset. (This version of f1imaeng does not need ax-rep nor ax-pow .) (Contributed by BTernaryTau, 13-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | f1imaen3g | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉 ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resexg | ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ↾ 𝐶 ) ∈ V ) | |
2 | 1 | 3ad2ant3 | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ↾ 𝐶 ) ∈ V ) |
3 | f1ores | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) | |
4 | 3 | 3adant3 | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) |
5 | f1oen3g | ⊢ ( ( ( 𝐹 ↾ 𝐶 ) ∈ V ∧ ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) ) | |
6 | 2 4 5 | syl2anc | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉 ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) ) |