This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐹 “ 𝐶 ) ≈ 𝐶 )