Theorem imasetpreimafvbij

Description: The mapping H is a bijective function between the set P of all preimages of values of function F and the range of F . (Contributed by AV, 22-Mar-2024)

	Ref	Expression
Hypotheses	fundcmpsurinj.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
	fundcmpsurinj.h	⊢ 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) )
Assertion	imasetpreimafvbij	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		fundcmpsurinj.h	⊢ 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) )
3	1 2	imasetpreimafvbijlemf1	⊢ ( 𝐹 Fn 𝐴 → 𝐻 : 𝑃 –1-1→ ( 𝐹 “ 𝐴 ) )
4	3	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 : 𝑃 –1-1→ ( 𝐹 “ 𝐴 ) )
5	1 2	imasetpreimafvbijlemfo	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 : 𝑃 –onto→ ( 𝐹 “ 𝐴 ) )
6		df-f1o	⊢ ( 𝐻 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐻 : 𝑃 –1-1→ ( 𝐹 “ 𝐴 ) ∧ 𝐻 : 𝑃 –onto→ ( 𝐹 “ 𝐴 ) ) )
7	4 5 6	sylanbrc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) )