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

Metamath Proof Explorer

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 eqtr3id ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐶 ) ) = 𝐶 )