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 bitrid ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐶 ⊆ ∩ ( 𝐹 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 𝐶 ⊆ ( 𝐹 ‘ 𝑥 ) ) )