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

Metamath Proof Explorer

Theorem imaf1homlem

Description: Lemma for imaf1hom and other theorems. (Contributed by Zhi Wang, 7-Nov-2025)

Ref Expression
Hypotheses imaf1hom.s ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
imaf1hom.1 ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ 𝐶 )
imaf1hom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
Assertion imaf1homlem ( 𝜑 → ( { ( ◡ 𝐹 ‘ 𝑋 ) } = ( ◡ 𝐹 “ { 𝑋 } ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 imaf1hom.s ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
2 imaf1hom.1 ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ 𝐶 )
3 imaf1hom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
4 f1f1orn ⊢ ( 𝐹 : 𝐵 –1-1→ 𝐶 → 𝐹 : 𝐵 –1-1-onto→ ran 𝐹 )
5 2 4 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ ran 𝐹 )
6 dff1o4 ⊢ ( 𝐹 : 𝐵 –1-1-onto→ ran 𝐹 ↔ ( 𝐹 Fn 𝐵 ∧ ◡ 𝐹 Fn ran 𝐹 ) )
7 6 simprbi ⊢ ( 𝐹 : 𝐵 –1-1-onto→ ran 𝐹 → ◡ 𝐹 Fn ran 𝐹 )
8 5 7 syl ⊢ ( 𝜑 → ◡ 𝐹 Fn ran 𝐹 )
9 imassrn ⊢ ( 𝐹 “ 𝐴 ) ⊆ ran 𝐹
10 3 1 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 “ 𝐴 ) )
11 9 10 sselid ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐹 )
12 fnsnfv ⊢ ( ( ◡ 𝐹 Fn ran 𝐹 ∧ 𝑋 ∈ ran 𝐹 ) → { ( ◡ 𝐹 ‘ 𝑋 ) } = ( ◡ 𝐹 “ { 𝑋 } ) )
13 8 11 12 syl2anc ⊢ ( 𝜑 → { ( ◡ 𝐹 ‘ 𝑋 ) } = ( ◡ 𝐹 “ { 𝑋 } ) )
14 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ ran 𝐹 ∧ 𝑋 ∈ ran 𝐹 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 )
15 5 11 14 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 )
16 f1ocnvdm ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ ran 𝐹 ∧ 𝑋 ∈ ran 𝐹 ) → ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
17 5 11 16 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
18 13 15 17 3jca ⊢ ( 𝜑 → ( { ( ◡ 𝐹 ‘ 𝑋 ) } = ( ◡ 𝐹 “ { 𝑋 } ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )