Metamath Proof Explorer

Theorem fnssintima

Description: Condition for subset of an intersection of an image. (Contributed by Scott Fenton, 16-Aug-2024)

Ref Expression
Assertion fnssintima ⊢ F Fn A ∧ B ⊆ A → C ⊆ ⋂ F B ↔ ∀ x ∈ B C ⊆ F ⁡ x

Proof

Step Hyp Ref Expression
1 ssint ⊢ C ⊆ ⋂ F B ↔ ∀ y ∈ F B C ⊆ y
2 df-ral ⊢ ∀ y ∈ F B C ⊆ y ↔ ∀ y y ∈ F B → C ⊆ y
3 1 2 bitri ⊢ C ⊆ ⋂ F B ↔ ∀ y y ∈ F B → C ⊆ y
4 fvelimab ⊢ F Fn A ∧ B ⊆ A → y ∈ F B ↔ ∃ x ∈ B F ⁡ x = y
5 4 imbi1d ⊢ F Fn A ∧ B ⊆ A → y ∈ F B → C ⊆ y ↔ ∃ x ∈ B F ⁡ x = y → C ⊆ y
6 5 albidv ⊢ F Fn A ∧ B ⊆ A → ∀ y y ∈ F B → C ⊆ y ↔ ∀ y ∃ x ∈ B F ⁡ x = y → C ⊆ y
7 ralcom4 ⊢ ∀ x ∈ B ∀ y F ⁡ x = y → C ⊆ y ↔ ∀ y ∀ x ∈ B F ⁡ x = y → C ⊆ y
8 eqcom ⊢ F ⁡ x = y ↔ y = F ⁡ x
9 8 imbi1i ⊢ F ⁡ x = y → C ⊆ y ↔ y = F ⁡ x → C ⊆ y
10 9 albii ⊢ ∀ y F ⁡ x = y → C ⊆ y ↔ ∀ y y = F ⁡ x → C ⊆ y
11 fvex ⊢ F ⁡ x ∈ V
12 sseq2 ⊢ y = F ⁡ x → C ⊆ y ↔ C ⊆ F ⁡ x
13 11 12 ceqsalv ⊢ ∀ y y = F ⁡ x → C ⊆ y ↔ C ⊆ F ⁡ x
14 10 13 bitri ⊢ ∀ y F ⁡ x = y → C ⊆ y ↔ C ⊆ F ⁡ x
15 14 ralbii ⊢ ∀ x ∈ B ∀ y F ⁡ x = y → C ⊆ y ↔ ∀ x ∈ B C ⊆ F ⁡ x
16 r19.23v ⊢ ∀ x ∈ B F ⁡ x = y → C ⊆ y ↔ ∃ x ∈ B F ⁡ x = y → C ⊆ y
17 16 albii ⊢ ∀ y ∀ x ∈ B F ⁡ x = y → C ⊆ y ↔ ∀ y ∃ x ∈ B F ⁡ x = y → C ⊆ y
18 7 15 17 3bitr3ri ⊢ ∀ y ∃ x ∈ B F ⁡ x = y → C ⊆ y ↔ ∀ x ∈ B C ⊆ F ⁡ x
19 6 18 bitrdi ⊢ F Fn A ∧ B ⊆ A → ∀ y y ∈ F B → C ⊆ y ↔ ∀ x ∈ B C ⊆ F ⁡ x
20 3 19 syl5bb ⊢ F Fn A ∧ B ⊆ A → C ⊆ ⋂ F B ↔ ∀ x ∈ B C ⊆ F ⁡ x