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