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

Proof

Step Hyp Ref Expression
1 ssint ⊢C⊆⋂FB↔∀y∈FBC⊆y
2 df-ral ⊢∀y∈FBC⊆y↔∀yy∈FB→C⊆y
3 1 2 bitri ⊢C⊆⋂FB↔∀yy∈FB→C⊆y
4 fvelimab ⊢FFnA∧B⊆A→y∈FB↔∃x∈BF⁡x=y
5 4 imbi1d ⊢FFnA∧B⊆A→y∈FB→C⊆y↔∃x∈BF⁡x=y→C⊆y
6 5 albidv ⊢FFnA∧B⊆A→∀yy∈FB→C⊆y↔∀y∃x∈BF⁡x=y→C⊆y
7 ralcom4 ⊢∀x∈B∀yF⁡x=y→C⊆y↔∀y∀x∈BF⁡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 ⊢∀yF⁡x=y→C⊆y↔∀yy=F⁡x→C⊆y
11 fvex ⊢F⁡x∈V
12 sseq2 ⊢y=F⁡x→C⊆y↔C⊆F⁡x
13 11 12 ceqsalv ⊢∀yy=F⁡x→C⊆y↔C⊆F⁡x
14 10 13 bitri ⊢∀yF⁡x=y→C⊆y↔C⊆F⁡x
15 14 ralbii ⊢∀x∈B∀yF⁡x=y→C⊆y↔∀x∈BC⊆F⁡x
16 r19.23v ⊢∀x∈BF⁡x=y→C⊆y↔∃x∈BF⁡x=y→C⊆y
17 16 albii ⊢∀y∀x∈BF⁡x=y→C⊆y↔∀y∃x∈BF⁡x=y→C⊆y
18 7 15 17 3bitr3ri ⊢∀y∃x∈BF⁡x=y→C⊆y↔∀x∈BC⊆F⁡x
19 6 18 bitrdi ⊢FFnA∧B⊆A→∀yy∈FB→C⊆y↔∀x∈BC⊆F⁡x
20 3 19 bitrid ⊢FFnA∧B⊆A→C⊆⋂FB↔∀x∈BC⊆F⁡x