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 ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝐶 ( 𝐹𝐵 ) ↔ ∀ 𝑥𝐵 𝐶 ⊆ ( 𝐹𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 ssint ( 𝐶 ( 𝐹𝐵 ) ↔ ∀ 𝑦 ∈ ( 𝐹𝐵 ) 𝐶𝑦 )
2 df-ral ( ∀ 𝑦 ∈ ( 𝐹𝐵 ) 𝐶𝑦 ↔ ∀ 𝑦 ( 𝑦 ∈ ( 𝐹𝐵 ) → 𝐶𝑦 ) )
3 1 2 bitri ( 𝐶 ( 𝐹𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ( 𝐹𝐵 ) → 𝐶𝑦 ) )
4 fvelimab ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝑦 ∈ ( 𝐹𝐵 ) ↔ ∃ 𝑥𝐵 ( 𝐹𝑥 ) = 𝑦 ) )
5 4 imbi1d ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝑦 ∈ ( 𝐹𝐵 ) → 𝐶𝑦 ) ↔ ( ∃ 𝑥𝐵 ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) ) )
6 5 albidv ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ∀ 𝑦 ( 𝑦 ∈ ( 𝐹𝐵 ) → 𝐶𝑦 ) ↔ ∀ 𝑦 ( ∃ 𝑥𝐵 ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) ) )
7 ralcom4 ( ∀ 𝑥𝐵𝑦 ( ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) ↔ ∀ 𝑦𝑥𝐵 ( ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) )
8 eqcom ( ( 𝐹𝑥 ) = 𝑦𝑦 = ( 𝐹𝑥 ) )
9 8 imbi1i ( ( ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) ↔ ( 𝑦 = ( 𝐹𝑥 ) → 𝐶𝑦 ) )
10 9 albii ( ∀ 𝑦 ( ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) ↔ ∀ 𝑦 ( 𝑦 = ( 𝐹𝑥 ) → 𝐶𝑦 ) )
11 fvex ( 𝐹𝑥 ) ∈ V
12 sseq2 ( 𝑦 = ( 𝐹𝑥 ) → ( 𝐶𝑦𝐶 ⊆ ( 𝐹𝑥 ) ) )
13 11 12 ceqsalv ( ∀ 𝑦 ( 𝑦 = ( 𝐹𝑥 ) → 𝐶𝑦 ) ↔ 𝐶 ⊆ ( 𝐹𝑥 ) )
14 10 13 bitri ( ∀ 𝑦 ( ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) ↔ 𝐶 ⊆ ( 𝐹𝑥 ) )
15 14 ralbii ( ∀ 𝑥𝐵𝑦 ( ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) ↔ ∀ 𝑥𝐵 𝐶 ⊆ ( 𝐹𝑥 ) )
16 r19.23v ( ∀ 𝑥𝐵 ( ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) ↔ ( ∃ 𝑥𝐵 ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) )
17 16 albii ( ∀ 𝑦𝑥𝐵 ( ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) ↔ ∀ 𝑦 ( ∃ 𝑥𝐵 ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) )
18 7 15 17 3bitr3ri ( ∀ 𝑦 ( ∃ 𝑥𝐵 ( 𝐹𝑥 ) = 𝑦𝐶𝑦 ) ↔ ∀ 𝑥𝐵 𝐶 ⊆ ( 𝐹𝑥 ) )
19 6 18 bitrdi ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ∀ 𝑦 ( 𝑦 ∈ ( 𝐹𝐵 ) → 𝐶𝑦 ) ↔ ∀ 𝑥𝐵 𝐶 ⊆ ( 𝐹𝑥 ) ) )
20 3 19 syl5bb ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝐶 ( 𝐹𝐵 ) ↔ ∀ 𝑥𝐵 𝐶 ⊆ ( 𝐹𝑥 ) ) )