Metamath Proof Explorer

Theorem f1elima

Description: Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion f1elima ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝑌 ) ↔ 𝑋 ∈ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 f1fn ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 Fn 𝐴 )
2 fvelimab ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝑌 ) ↔ ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) ) )
3 1 2 sylan ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝑌 ) ↔ ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) ) )
4 3 3adant2 ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝑌 ) ↔ ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) ) )
5 ssel ⊢ ( 𝑌 ⊆ 𝐴 → ( 𝑧 ∈ 𝑌 → 𝑧 ∈ 𝐴 ) )
6 5 impac ⊢ ( ( 𝑌 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑌 ) → ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑌 ) )
7 f1fveq ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) ↔ 𝑧 = 𝑋 ) )
8 7 ancom2s ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) ↔ 𝑧 = 𝑋 ) )
9 8 biimpd ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) → 𝑧 = 𝑋 ) )
10 9 anassrs ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) → 𝑧 = 𝑋 ) )
11 eleq1 ⊢ ( 𝑧 = 𝑋 → ( 𝑧 ∈ 𝑌 ↔ 𝑋 ∈ 𝑌 ) )
12 11 biimpcd ⊢ ( 𝑧 ∈ 𝑌 → ( 𝑧 = 𝑋 → 𝑋 ∈ 𝑌 ) )
13 10 12 sylan9 ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ 𝑌 ) )
14 13 anasss ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ 𝑌 ) )
15 6 14 sylan2 ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑌 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ 𝑌 ) )
16 15 anassrs ⊢ ( ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑧 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ 𝑌 ) )
17 16 rexlimdva ⊢ ( ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ⊆ 𝐴 ) → ( ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ 𝑌 ) )
18 17 3impa ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ 𝑌 ) )
19 eqid ⊢ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 )
20 fveqeq2 ⊢ ( 𝑧 = 𝑋 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) ) )
21 20 rspcev ⊢ ( ( 𝑋 ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) ) → ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) )
22 19 21 mpan2 ⊢ ( 𝑋 ∈ 𝑌 → ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) )
23 18 22 impbid1 ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) ↔ 𝑋 ∈ 𝑌 ) )
24 4 23 bitrd ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝑌 ) ↔ 𝑋 ∈ 𝑌 ) )