Theorem imasetpreimafvbijlemf

Description: Lemma for imasetpreimafvbij : the mapping H is a function into the range of function F . (Contributed by AV, 22-Mar-2024)

	Ref	Expression
Hypotheses	fundcmpsurinj.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
	fundcmpsurinj.h	⊢ 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) )
Assertion	imasetpreimafvbijlemf	⊢ ( 𝐹 Fn 𝐴 → 𝐻 : 𝑃 ⟶ ( 𝐹 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		fundcmpsurinj.h	⊢ 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) )
3	1	uniimaelsetpreimafv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑝 ∈ 𝑃 ) → ∪ ( 𝐹 “ 𝑝 ) ∈ ran 𝐹 )
4		fnima	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) = ran 𝐹 )
5	4	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑝 ∈ 𝑃 ) → ( 𝐹 “ 𝐴 ) = ran 𝐹 )
6	3 5	eleqtrrd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑝 ∈ 𝑃 ) → ∪ ( 𝐹 “ 𝑝 ) ∈ ( 𝐹 “ 𝐴 ) )
7	6 2	fmptd	⊢ ( 𝐹 Fn 𝐴 → 𝐻 : 𝑃 ⟶ ( 𝐹 “ 𝐴 ) )