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

Metamath Proof Explorer

Theorem f1ssf1

Description: A subset of an injective function is injective. (Contributed by AV, 20-Nov-2020)

Ref Expression
Assertion f1ssf1 ( ( Fun 𝐹 ∧ Fun ◡ 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → Fun ◡ 𝐺 )

Proof

Step Hyp Ref Expression
1 funssres ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 )
2 funres11 ⊢ ( Fun ◡ 𝐹 → Fun ◡ ( 𝐹 ↾ dom 𝐺 ) )
3 cnveq ⊢ ( 𝐺 = ( 𝐹 ↾ dom 𝐺 ) → ◡ 𝐺 = ◡ ( 𝐹 ↾ dom 𝐺 ) )
4 3 funeqd ⊢ ( 𝐺 = ( 𝐹 ↾ dom 𝐺 ) → ( Fun ◡ 𝐺 ↔ Fun ◡ ( 𝐹 ↾ dom 𝐺 ) ) )
5 2 4 imbitrrid ⊢ ( 𝐺 = ( 𝐹 ↾ dom 𝐺 ) → ( Fun ◡ 𝐹 → Fun ◡ 𝐺 ) )
6 5 eqcoms ⊢ ( ( 𝐹 ↾ dom 𝐺 ) = 𝐺 → ( Fun ◡ 𝐹 → Fun ◡ 𝐺 ) )
7 1 6 syl ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( Fun ◡ 𝐹 → Fun ◡ 𝐺 ) )
8 7 ex ⊢ ( Fun 𝐹 → ( 𝐺 ⊆ 𝐹 → ( Fun ◡ 𝐹 → Fun ◡ 𝐺 ) ) )
9 8 com23 ⊢ ( Fun 𝐹 → ( Fun ◡ 𝐹 → ( 𝐺 ⊆ 𝐹 → Fun ◡ 𝐺 ) ) )
10 9 3imp ⊢ ( ( Fun 𝐹 ∧ Fun ◡ 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → Fun ◡ 𝐺 )