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 ⁡ F ∧ A ⊆ dom ⁡ F → F A ⊆ B ↔ A ⊆ F -1 B

Proof

Step Hyp Ref Expression
1 funimass4 ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → F A ⊆ B ↔ ∀ x ∈ A F ⁡ x ∈ B
2 ssel ⊢ A ⊆ dom ⁡ F → x ∈ A → x ∈ dom ⁡ F
3 fvimacnv ⊢ Fun ⁡ F ∧ x ∈ dom ⁡ F → F ⁡ x ∈ B ↔ x ∈ F -1 B
4 3 ex ⊢ Fun ⁡ F → x ∈ dom ⁡ F → F ⁡ x ∈ B ↔ x ∈ F -1 B
5 2 4 syl9r ⊢ Fun ⁡ F → A ⊆ dom ⁡ F → x ∈ A → F ⁡ x ∈ B ↔ x ∈ F -1 B
6 5 imp31 ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F ∧ x ∈ A → F ⁡ x ∈ B ↔ x ∈ F -1 B
7 6 ralbidva ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → ∀ x ∈ A F ⁡ x ∈ B ↔ ∀ x ∈ A x ∈ F -1 B
8 1 7 bitrd ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → F A ⊆ B ↔ ∀ x ∈ A x ∈ F -1 B
9 dfss3 ⊢ A ⊆ F -1 B ↔ ∀ x ∈ A x ∈ F -1 B
10 8 9 bitr4di ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → F A ⊆ B ↔ A ⊆ F -1 B