Theorem imasetpreimafvbijlemfv

Description: Lemma for imasetpreimafvbij : the value of the mapping H at a preimage of a value of function F . (Contributed by AV, 5-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		fundcmpsurinj.h	⊢ 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) )
3		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
4	3	anim1i	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ) → ( Fun 𝐹 ∧ 𝑌 ∈ 𝑃 ) )
5	4	3adant3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) → ( Fun 𝐹 ∧ 𝑌 ∈ 𝑃 ) )
6	1 2	fundcmpsurinjlem3	⊢ ( ( Fun 𝐹 ∧ 𝑌 ∈ 𝑃 ) → ( 𝐻 ‘ 𝑌 ) = ∪ ( 𝐹 “ 𝑌 ) )
7	5 6	syl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) → ( 𝐻 ‘ 𝑌 ) = ∪ ( 𝐹 “ 𝑌 ) )
8	3	3ad2ant1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) → Fun 𝐹 )
9		funiunfv	⊢ ( Fun 𝐹 → ∪ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = ∪ ( 𝐹 “ 𝑌 ) )
10	8 9	syl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) → ∪ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = ∪ ( 𝐹 “ 𝑌 ) )
11		simp3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) → 𝑋 ∈ 𝑌 )
12		simpl1	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐹 Fn 𝐴 )
13		simpl2	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑌 ∈ 𝑃 )
14		simpr	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
15		simpl3	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑋 ∈ 𝑌 )
16	1	elsetpreimafveqfv	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑌 ∈ 𝑃 ∧ 𝑦 ∈ 𝑌 ∧ 𝑋 ∈ 𝑌 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
17	12 13 14 15 16	syl13anc	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
18	17	ralrimiva	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) → ∀ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
19		fveq2	⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
20	19	iuneqconst	⊢ ( ( 𝑋 ∈ 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) → ∪ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
21	11 18 20	syl2anc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) → ∪ 𝑦 ∈ 𝑌 ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
22	7 10 21	3eqtr2d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌 ) → ( 𝐻 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) )