Metamath Proof Explorer

Theorem f1imass

Description: Taking images under a one-to-one function preserves subsets. (Contributed by Stefan O'Rear, 30-Oct-2014)

Ref Expression
Assertion f1imass ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ↔ 𝐶 ⊆ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 simplrl ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) → 𝐶 ⊆ 𝐴 )
2 1 sseld ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) → ( 𝑎 ∈ 𝐶 → 𝑎 ∈ 𝐴 ) )
3 simplr ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) )
4 3 sseld ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐶 ) → ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐷 ) ) )
5 simplll ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
6 simpr ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
7 simp1rl ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ∧ 𝑎 ∈ 𝐴 ) → 𝐶 ⊆ 𝐴 )
8 7 3expa ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐶 ⊆ 𝐴 )
9 f1elima ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑎 ∈ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐶 ) ↔ 𝑎 ∈ 𝐶 ) )
10 5 6 8 9 syl3anc ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐶 ) ↔ 𝑎 ∈ 𝐶 ) )
11 simp1rr ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ∧ 𝑎 ∈ 𝐴 ) → 𝐷 ⊆ 𝐴 )
12 11 3expa ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐷 ⊆ 𝐴 )
13 f1elima ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑎 ∈ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐷 ) ↔ 𝑎 ∈ 𝐷 ) )
14 5 6 12 13 syl3anc ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐷 ) ↔ 𝑎 ∈ 𝐷 ) )
15 4 10 14 3imtr3d ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ∈ 𝐶 → 𝑎 ∈ 𝐷 ) )
16 15 ex ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) → ( 𝑎 ∈ 𝐴 → ( 𝑎 ∈ 𝐶 → 𝑎 ∈ 𝐷 ) ) )
17 2 16 syld ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) → ( 𝑎 ∈ 𝐶 → ( 𝑎 ∈ 𝐶 → 𝑎 ∈ 𝐷 ) ) )
18 17 pm2.43d ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) → ( 𝑎 ∈ 𝐶 → 𝑎 ∈ 𝐷 ) )
19 18 ssrdv ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ) → 𝐶 ⊆ 𝐷 )
20 19 ex ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) → 𝐶 ⊆ 𝐷 ) )
21 imass2 ⊢ ( 𝐶 ⊆ 𝐷 → ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) )
22 20 21 impbid1 ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ↔ 𝐶 ⊆ 𝐷 ) )