Theorem imasetpreimafvbijlemfv1

Description: Lemma for imasetpreimafvbij : for a preimage of a value of function F there is an element of the preimage so that the value of the mapping H at this preimage is the function value at this element. (Contributed by AV, 5-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		fundcmpsurinj.h	⊢ 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) )
3	1	0nelsetpreimafv	⊢ ( 𝐹 Fn 𝐴 → ∅ ∉ 𝑃 )
4		elnelne2	⊢ ( ( 𝑋 ∈ 𝑃 ∧ ∅ ∉ 𝑃 ) → 𝑋 ≠ ∅ )
5	4	expcom	⊢ ( ∅ ∉ 𝑃 → ( 𝑋 ∈ 𝑃 → 𝑋 ≠ ∅ ) )
6	3 5	syl	⊢ ( 𝐹 Fn 𝐴 → ( 𝑋 ∈ 𝑃 → 𝑋 ≠ ∅ ) )
7	6	imp	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ≠ ∅ )
8		simpr	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
9	1 2	imasetpreimafvbijlemfv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐻 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) )
10	9	3expa	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐻 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) )
11	8 10	jca	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑋 ∧ ( 𝐻 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ) )
12	11	ex	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃 ) → ( 𝑦 ∈ 𝑋 → ( 𝑦 ∈ 𝑋 ∧ ( 𝐻 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
13	12	eximdv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃 ) → ( ∃ 𝑦 𝑦 ∈ 𝑋 → ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ ( 𝐻 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
14		n0	⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑋 )
15		df-rex	⊢ ( ∃ 𝑦 ∈ 𝑋 ( 𝐻 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ ( 𝐻 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ) )
16	13 14 15	3imtr4g	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃 ) → ( 𝑋 ≠ ∅ → ∃ 𝑦 ∈ 𝑋 ( 𝐻 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ) )
17	7 16	mpd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃 ) → ∃ 𝑦 ∈ 𝑋 ( 𝐻 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) )