This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1imapss

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

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

Proof

Step Hyp Ref Expression
1 f1imass ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ↔ 𝐶 ⊆ 𝐷 ) )
2 f1imaeq ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) = ( 𝐹 “ 𝐷 ) ↔ 𝐶 = 𝐷 ) )
3 2 notbid ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ¬ ( 𝐹 “ 𝐶 ) = ( 𝐹 “ 𝐷 ) ↔ ¬ 𝐶 = 𝐷 ) )
4 1 3 anbi12d ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ∧ ¬ ( 𝐹 “ 𝐶 ) = ( 𝐹 “ 𝐷 ) ) ↔ ( 𝐶 ⊆ 𝐷 ∧ ¬ 𝐶 = 𝐷 ) ) )
5 dfpss2 ⊢ ( ( 𝐹 “ 𝐶 ) ⊊ ( 𝐹 “ 𝐷 ) ↔ ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ∧ ¬ ( 𝐹 “ 𝐶 ) = ( 𝐹 “ 𝐷 ) ) )
6 dfpss2 ⊢ ( 𝐶 ⊊ 𝐷 ↔ ( 𝐶 ⊆ 𝐷 ∧ ¬ 𝐶 = 𝐷 ) )
7 4 5 6 3bitr4g ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) ⊊ ( 𝐹 “ 𝐷 ) ↔ 𝐶 ⊊ 𝐷 ) )