Theorem f1imacnv

Description: Preimage of an image. (Contributed by NM, 30-Sep-2004)

	Ref	Expression
Assertion	f1imacnv	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐶 ) ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		resima	⊢ ( ( ◡ 𝐹 ↾ ( 𝐹 “ 𝐶 ) ) “ ( 𝐹 “ 𝐶 ) ) = ( ◡ 𝐹 “ ( 𝐹 “ 𝐶 ) )
2		df-f1	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) )
3	2	simprbi	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Fun ◡ 𝐹 )
4	3	adantr	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → Fun ◡ 𝐹 )
5		funcnvres	⊢ ( Fun ◡ 𝐹 → ◡ ( 𝐹 ↾ 𝐶 ) = ( ◡ 𝐹 ↾ ( 𝐹 “ 𝐶 ) ) )
6	4 5	syl	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ◡ ( 𝐹 ↾ 𝐶 ) = ( ◡ 𝐹 ↾ ( 𝐹 “ 𝐶 ) ) )
7	6	imaeq1d	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ◡ ( 𝐹 ↾ 𝐶 ) “ ( 𝐹 “ 𝐶 ) ) = ( ( ◡ 𝐹 ↾ ( 𝐹 “ 𝐶 ) ) “ ( 𝐹 “ 𝐶 ) ) )
8		f1ores	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) )
9		f1ocnv	⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐹 “ 𝐶 ) → ◡ ( 𝐹 ↾ 𝐶 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 )
10	8 9	syl	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ◡ ( 𝐹 ↾ 𝐶 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 )
11		imadmrn	⊢ ( ◡ ( 𝐹 ↾ 𝐶 ) “ dom ◡ ( 𝐹 ↾ 𝐶 ) ) = ran ◡ ( 𝐹 ↾ 𝐶 )
12		f1odm	⊢ ( ◡ ( 𝐹 ↾ 𝐶 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 → dom ◡ ( 𝐹 ↾ 𝐶 ) = ( 𝐹 “ 𝐶 ) )
13	12	imaeq2d	⊢ ( ◡ ( 𝐹 ↾ 𝐶 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 → ( ◡ ( 𝐹 ↾ 𝐶 ) “ dom ◡ ( 𝐹 ↾ 𝐶 ) ) = ( ◡ ( 𝐹 ↾ 𝐶 ) “ ( 𝐹 “ 𝐶 ) ) )
14		f1ofo	⊢ ( ◡ ( 𝐹 ↾ 𝐶 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 → ◡ ( 𝐹 ↾ 𝐶 ) : ( 𝐹 “ 𝐶 ) –onto→ 𝐶 )
15		forn	⊢ ( ◡ ( 𝐹 ↾ 𝐶 ) : ( 𝐹 “ 𝐶 ) –onto→ 𝐶 → ran ◡ ( 𝐹 ↾ 𝐶 ) = 𝐶 )
16	14 15	syl	⊢ ( ◡ ( 𝐹 ↾ 𝐶 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 → ran ◡ ( 𝐹 ↾ 𝐶 ) = 𝐶 )
17	11 13 16	3eqtr3a	⊢ ( ◡ ( 𝐹 ↾ 𝐶 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 → ( ◡ ( 𝐹 ↾ 𝐶 ) “ ( 𝐹 “ 𝐶 ) ) = 𝐶 )
18	10 17	syl	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ◡ ( 𝐹 ↾ 𝐶 ) “ ( 𝐹 “ 𝐶 ) ) = 𝐶 )
19	7 18	eqtr3d	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ( ◡ 𝐹 ↾ ( 𝐹 “ 𝐶 ) ) “ ( 𝐹 “ 𝐶 ) ) = 𝐶 )
20	1 19	syl5eqr	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐶 ) ) = 𝐶 )