Theorem fundcmpsurinjlem3

Description: Lemma 3 for fundcmpsurinj . (Contributed by AV, 3-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		fundcmpsurinj.h	⊢ 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) )
3	2	a1i	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ 𝑃 ) → 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) ) )
4		imaeq2	⊢ ( 𝑝 = 𝑋 → ( 𝐹 “ 𝑝 ) = ( 𝐹 “ 𝑋 ) )
5	4	unieqd	⊢ ( 𝑝 = 𝑋 → ∪ ( 𝐹 “ 𝑝 ) = ∪ ( 𝐹 “ 𝑋 ) )
6	5	adantl	⊢ ( ( ( Fun 𝐹 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 = 𝑋 ) → ∪ ( 𝐹 “ 𝑝 ) = ∪ ( 𝐹 “ 𝑋 ) )
7		simpr	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ∈ 𝑃 )
8		funimaexg	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ 𝑃 ) → ( 𝐹 “ 𝑋 ) ∈ V )
9	8	uniexd	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ 𝑃 ) → ∪ ( 𝐹 “ 𝑋 ) ∈ V )
10	3 6 7 9	fvmptd	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ 𝑃 ) → ( 𝐻 ‘ 𝑋 ) = ∪ ( 𝐹 “ 𝑋 ) )