Theorem f1elima 7300

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

Assertion

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

Proof of Theorem f1elima

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1fn 6818	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		fvelimab 6994	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋)))
3	1, 2	sylan 579	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋)))
4	3	3adant2 1131	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋)))
5		ssel 4002	. . . . . . . 8 ⊢ (𝑌 ⊆ 𝐴 → (𝑧 ∈ 𝑌 → 𝑧 ∈ 𝐴))
6	5	impac 552	. . . . . . 7 ⊢ ((𝑌 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑌) → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑌))
7		f1fveq 7299	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑧 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐹‘𝑧) = (𝐹‘𝑋) ↔ 𝑧 = 𝑋))
8	7	ancom2s 649	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) = (𝐹‘𝑋) ↔ 𝑧 = 𝑋))
9	8	biimpd 229	. . . . . . . . . 10 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑧 = 𝑋))
10	9	anassrs 467	. . . . . . . . 9 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑧 = 𝑋))
11		eleq1 2832	. . . . . . . . . 10 ⊢ (𝑧 = 𝑋 → (𝑧 ∈ 𝑌 ↔ 𝑋 ∈ 𝑌))
12	11	biimpcd 249	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝑌 → (𝑧 = 𝑋 → 𝑋 ∈ 𝑌))
13	10, 12	sylan9 507	. . . . . . . 8 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ∈ 𝑌) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌))
14	13	anasss 466	. . . . . . 7 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌))
15	6, 14	sylan2 592	. . . . . 6 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ (𝑌 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌))
16	15	anassrs 467	. . . . 5 ⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ⊆ 𝐴) ∧ 𝑧 ∈ 𝑌) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌))
17	16	rexlimdva 3161	. . . 4 ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ⊆ 𝐴) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌))
18	17	3impa 1110	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌))
19		eqid 2740	. . . 4 ⊢ (𝐹‘𝑋) = (𝐹‘𝑋)
20		fveqeq2 6929	. . . . 5 ⊢ (𝑧 = 𝑋 → ((𝐹‘𝑧) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = (𝐹‘𝑋)))
21	20	rspcev 3635	. . . 4 ⊢ ((𝑋 ∈ 𝑌 ∧ (𝐹‘𝑋) = (𝐹‘𝑋)) → ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋))
22	19, 21	mpan2 690	. . 3 ⊢ (𝑋 ∈ 𝑌 → ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋))
23	18, 22	impbid1 225	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋) ↔ 𝑋 ∈ 𝑌))
24	4, 23	bitrd 279	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ 𝑋 ∈ 𝑌))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ∃wrex 3076   ⊆ wss 3976   “ cima 5703   Fn wfn 6568  –1-1→wf1 6570  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fv 6581

This theorem is referenced by:  f1imass  7301  domunfican  9389  acndom2  10123  hashf1lem1  14504  f1omvdconj  19488  gsumzaddlem  19963  lindfmm  21870  axcontlem10  29006  trlsegvdeg  30259  ismtyima  37763