Metamath Proof Explorer


Theorem funALTVss

Description: Subclass theorem for function. (Contributed by NM, 16-Aug-1994) (Proof shortened by Mario Carneiro, 24-Jun-2014) (Revised by Peter Mazsa, 22-Sep-2021)

Ref Expression
Assertion funALTVss ( 𝐴𝐵 → ( FunALTV 𝐵 → FunALTV 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cossss ( 𝐴𝐵 → ≀ 𝐴 ⊆ ≀ 𝐵 )
2 sstr2 ( ≀ 𝐴 ⊆ ≀ 𝐵 → ( ≀ 𝐵 ⊆ I → ≀ 𝐴 ⊆ I ) )
3 1 2 syl ( 𝐴𝐵 → ( ≀ 𝐵 ⊆ I → ≀ 𝐴 ⊆ I ) )
4 relss ( 𝐴𝐵 → ( Rel 𝐵 → Rel 𝐴 ) )
5 3 4 anim12d ( 𝐴𝐵 → ( ( ≀ 𝐵 ⊆ I ∧ Rel 𝐵 ) → ( ≀ 𝐴 ⊆ I ∧ Rel 𝐴 ) ) )
6 dffunALTV2 ( FunALTV 𝐵 ↔ ( ≀ 𝐵 ⊆ I ∧ Rel 𝐵 ) )
7 dffunALTV2 ( FunALTV 𝐴 ↔ ( ≀ 𝐴 ⊆ I ∧ Rel 𝐴 ) )
8 5 6 7 3imtr4g ( 𝐴𝐵 → ( FunALTV 𝐵 → FunALTV 𝐴 ) )