Metamath Proof Explorer


Theorem funimass3

Description: A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv would be the special case of A being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion funimass3 ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹𝐴 ) ⊆ 𝐵𝐴 ⊆ ( 𝐹𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 funimass4 ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 ) )
2 ssel ( 𝐴 ⊆ dom 𝐹 → ( 𝑥𝐴𝑥 ∈ dom 𝐹 ) )
3 fvimacnv ( ( Fun 𝐹𝑥 ∈ dom 𝐹 ) → ( ( 𝐹𝑥 ) ∈ 𝐵𝑥 ∈ ( 𝐹𝐵 ) ) )
4 3 ex ( Fun 𝐹 → ( 𝑥 ∈ dom 𝐹 → ( ( 𝐹𝑥 ) ∈ 𝐵𝑥 ∈ ( 𝐹𝐵 ) ) ) )
5 2 4 syl9r ( Fun 𝐹 → ( 𝐴 ⊆ dom 𝐹 → ( 𝑥𝐴 → ( ( 𝐹𝑥 ) ∈ 𝐵𝑥 ∈ ( 𝐹𝐵 ) ) ) ) )
6 5 imp31 ( ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) ∧ 𝑥𝐴 ) → ( ( 𝐹𝑥 ) ∈ 𝐵𝑥 ∈ ( 𝐹𝐵 ) ) )
7 6 ralbidva ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 ↔ ∀ 𝑥𝐴 𝑥 ∈ ( 𝐹𝐵 ) ) )
8 1 7 bitrd ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥𝐴 𝑥 ∈ ( 𝐹𝐵 ) ) )
9 dfss3 ( 𝐴 ⊆ ( 𝐹𝐵 ) ↔ ∀ 𝑥𝐴 𝑥 ∈ ( 𝐹𝐵 ) )
10 8 9 bitr4di ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹𝐴 ) ⊆ 𝐵𝐴 ⊆ ( 𝐹𝐵 ) ) )