Theorem uniimafveqt

Description: The union of the image of a subset S of the domain of a function with elements having the same function value is the function value at one of the elements of S . (Contributed by AV, 5-Mar-2024)

	Ref	Expression
Assertion	uniimafveqt	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ∪ ( 𝐹 “ 𝑆 ) = ( 𝐹 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ffun	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )
2	1	3ad2ant1	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → Fun 𝐹 )
3	2	adantr	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) → Fun 𝐹 )
4		funiunfv	⊢ ( Fun 𝐹 → ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) = ∪ ( 𝐹 “ 𝑆 ) )
5	3 4	syl	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) → ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) = ∪ ( 𝐹 “ 𝑆 ) )
6		simp3	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
7		fveqeq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) )
8	7	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
9	8	biimpi	⊢ ( ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ∀ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
10		fveq2	⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
11	10	iuneqconst	⊢ ( ( 𝑋 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) → ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
12	6 9 11	syl2an	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) → ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
13	5 12	eqtr3d	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) → ∪ ( 𝐹 “ 𝑆 ) = ( 𝐹 ‘ 𝑋 ) )
14	13	ex	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ∪ ( 𝐹 “ 𝑆 ) = ( 𝐹 ‘ 𝑋 ) ) )