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	⊢ ( 𝜑 → ( { ( ◡ 𝐹 ‘ 𝑋 ) } = ( ◡ 𝐹 “ { 𝑋 } ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )