Theorem fnfvintima

Description: Condition for a function value to equal the intersection of an image that contains it. (Contributed by BTernaryTau, 23-Jun-2026)

	Ref	Expression
Assertion	fnfvintima	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐶 ) = ∩ ( 𝐹 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqimss	⊢ ( ( 𝐹 ‘ 𝐶 ) = ∩ ( 𝐹 “ 𝐵 ) → ( 𝐹 ‘ 𝐶 ) ⊆ ∩ ( 𝐹 “ 𝐵 ) )
2		fnssintima	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ‘ 𝐶 ) ⊆ ∩ ( 𝐹 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
3	2	3adant3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐶 ) ⊆ ∩ ( 𝐹 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
4	1 3	imbitrid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐶 ) = ∩ ( 𝐹 “ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
5	3	biimprd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝐶 ) ⊆ ∩ ( 𝐹 “ 𝐵 ) ) )
6		fnfvima	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 “ 𝐵 ) )
7		intss1	⊢ ( ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 “ 𝐵 ) → ∩ ( 𝐹 “ 𝐵 ) ⊆ ( 𝐹 ‘ 𝐶 ) )
8	6 7	syl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ∩ ( 𝐹 “ 𝐵 ) ⊆ ( 𝐹 ‘ 𝐶 ) )
9	5 8	jctird	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝐶 ) ⊆ ∩ ( 𝐹 “ 𝐵 ) ∧ ∩ ( 𝐹 “ 𝐵 ) ⊆ ( 𝐹 ‘ 𝐶 ) ) ) )
10		eqss	⊢ ( ( 𝐹 ‘ 𝐶 ) = ∩ ( 𝐹 “ 𝐵 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ⊆ ∩ ( 𝐹 “ 𝐵 ) ∧ ∩ ( 𝐹 “ 𝐵 ) ⊆ ( 𝐹 ‘ 𝐶 ) ) )
11	9 10	imbitrrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝐶 ) = ∩ ( 𝐹 “ 𝐵 ) ) )
12	4 11	impbid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐶 ) = ∩ ( 𝐹 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )