Theorem f1imaen2g

Description: If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (This version of f1imaeng does not need ax-rep .) (Contributed by Mario Carneiro, 16-Nov-2014) (Revised by Mario Carneiro, 25-Jun-2015)

	Ref	Expression
Assertion	f1imaen2g	⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		simprr	⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
2		simplr	⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
3		f1f	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
4		fimass	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 “ 𝐶 ) ⊆ 𝐵 )
5	3 4	syl	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝐹 “ 𝐶 ) ⊆ 𝐵 )
6	5	ad2antrr	⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐹 “ 𝐶 ) ⊆ 𝐵 )
7	2 6	ssexd	⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐹 “ 𝐶 ) ∈ V )
8		f1ores	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) )
9	8	ad2ant2r	⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) )
10		f1oen2g	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐹 “ 𝐶 ) ∈ V ∧ ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) )
11	1 7 9 10	syl3anc	⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ≈ ( 𝐹 “ 𝐶 ) )
12	11	ensymd	⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )