Metamath Proof Explorer


Theorem disjss

Description: Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020) (Revised by Peter Mazsa, 22-Sep-2021)

Ref Expression
Assertion disjss ( 𝐴𝐵 → ( Disj 𝐵 → Disj 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cnvss ( 𝐴𝐵 𝐴 𝐵 )
2 funALTVss ( 𝐴 𝐵 → ( FunALTV 𝐵 → FunALTV 𝐴 ) )
3 1 2 syl ( 𝐴𝐵 → ( FunALTV 𝐵 → FunALTV 𝐴 ) )
4 relss ( 𝐴𝐵 → ( Rel 𝐵 → Rel 𝐴 ) )
5 3 4 anim12d ( 𝐴𝐵 → ( ( FunALTV 𝐵 ∧ Rel 𝐵 ) → ( FunALTV 𝐴 ∧ Rel 𝐴 ) ) )
6 dfdisjALTV ( Disj 𝐵 ↔ ( FunALTV 𝐵 ∧ Rel 𝐵 ) )
7 dfdisjALTV ( Disj 𝐴 ↔ ( FunALTV 𝐴 ∧ Rel 𝐴 ) )
8 5 6 7 3imtr4g ( 𝐴𝐵 → ( Disj 𝐵 → Disj 𝐴 ) )