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 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) ) )