Metamath Proof Explorer

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 ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ B → F ⁡ C = ⋂ F B ↔ ∀ x ∈ B F ⁡ C ⊆ F ⁡ x

Proof

Step Hyp Ref Expression
1 eqimss ⊢ F ⁡ C = ⋂ F B → F ⁡ C ⊆ ⋂ F B
2 fnssintima ⊢ F Fn A ∧ B ⊆ A → F ⁡ C ⊆ ⋂ F B ↔ ∀ x ∈ B F ⁡ C ⊆ F ⁡ x
3 2 3adant3 ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ B → F ⁡ C ⊆ ⋂ F B ↔ ∀ x ∈ B F ⁡ C ⊆ F ⁡ x
4 1 3 imbitrid ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ B → F ⁡ C = ⋂ F B → ∀ x ∈ B F ⁡ C ⊆ F ⁡ x
5 3 biimprd ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ B → ∀ x ∈ B F ⁡ C ⊆ F ⁡ x → F ⁡ C ⊆ ⋂ F B
6 fnfvima ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ B → F ⁡ C ∈ F B
7 intss1 ⊢ F ⁡ C ∈ F B → ⋂ F B ⊆ F ⁡ C
8 6 7 syl ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ B → ⋂ F B ⊆ F ⁡ C
9 5 8 jctird ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ B → ∀ x ∈ B F ⁡ C ⊆ F ⁡ x → F ⁡ C ⊆ ⋂ F B ∧ ⋂ F B ⊆ F ⁡ C
10 eqss ⊢ F ⁡ C = ⋂ F B ↔ F ⁡ C ⊆ ⋂ F B ∧ ⋂ F B ⊆ F ⁡ C
11 9 10 imbitrrdi ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ B → ∀ x ∈ B F ⁡ C ⊆ F ⁡ x → F ⁡ C = ⋂ F B
12 4 11 impbid ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ B → F ⁡ C = ⋂ F B ↔ ∀ x ∈ B F ⁡ C ⊆ F ⁡ x