Step | Hyp | Ref
| Expression |
1 | | fvmpt2.1 |
. . . . 5
⊢ F = (x ∈ A ↦ B) |
2 | 1 | dmmptss 5685 |
. . . 4
⊢ dom F ⊆ A |
3 | 2 | sseli 3269 |
. . 3
⊢ (D ∈ dom F → D ∈ A) |
4 | | fveq2 5328 |
. . . . . . 7
⊢ (y = D →
(F ‘y) = (F
‘D)) |
5 | 4 | sseq1d 3298 |
. . . . . 6
⊢ (y = D →
((F ‘y) ⊆ C ↔ (F
‘D) ⊆ C)) |
6 | 5 | imbi2d 307 |
. . . . 5
⊢ (y = D →
((∀x
∈ A
B ⊆
C → (F ‘y)
⊆ C)
↔ (∀x ∈ A B ⊆ C →
(F ‘D) ⊆ C))) |
7 | | nfcv 2489 |
. . . . . 6
⊢
Ⅎxy |
8 | | nfra1 2664 |
. . . . . . 7
⊢ Ⅎx∀x ∈ A B ⊆ C |
9 | | nfmpt1 5672 |
. . . . . . . . . 10
⊢
Ⅎx(x ∈ A ↦ B) |
10 | 1, 9 | nfcxfr 2486 |
. . . . . . . . 9
⊢
ℲxF |
11 | 10, 7 | nffv 5334 |
. . . . . . . 8
⊢
Ⅎx(F ‘y) |
12 | | nfcv 2489 |
. . . . . . . 8
⊢
ℲxC |
13 | 11, 12 | nfss 3266 |
. . . . . . 7
⊢ Ⅎx(F
‘y) ⊆ C |
14 | 8, 13 | nfim 1813 |
. . . . . 6
⊢ Ⅎx(∀x ∈ A B ⊆ C →
(F ‘y) ⊆ C) |
15 | | fveq2 5328 |
. . . . . . . 8
⊢ (x = y →
(F ‘x) = (F
‘y)) |
16 | 15 | sseq1d 3298 |
. . . . . . 7
⊢ (x = y →
((F ‘x) ⊆ C ↔ (F
‘y) ⊆ C)) |
17 | 16 | imbi2d 307 |
. . . . . 6
⊢ (x = y →
((∀x
∈ A
B ⊆
C → (F ‘x)
⊆ C)
↔ (∀x ∈ A B ⊆ C →
(F ‘y) ⊆ C))) |
18 | 1 | dmmpt 5683 |
. . . . . . . . . . 11
⊢ dom F = {x ∈ A ∣ B ∈ V} |
19 | 18 | rabeq2i 2856 |
. . . . . . . . . 10
⊢ (x ∈ dom F ↔ (x
∈ A ∧ B ∈ V)) |
20 | 1 | fvmpt2 5704 |
. . . . . . . . . . 11
⊢ ((x ∈ A ∧ B ∈ V) →
(F ‘x) = B) |
21 | | eqimss 3323 |
. . . . . . . . . . 11
⊢ ((F ‘x) =
B → (F ‘x)
⊆ B) |
22 | 20, 21 | syl 15 |
. . . . . . . . . 10
⊢ ((x ∈ A ∧ B ∈ V) →
(F ‘x) ⊆ B) |
23 | 19, 22 | sylbi 187 |
. . . . . . . . 9
⊢ (x ∈ dom F → (F
‘x) ⊆ B) |
24 | | ndmfv 5349 |
. . . . . . . . . 10
⊢ (¬ x ∈ dom F → (F
‘x) = ∅) |
25 | | 0ss 3579 |
. . . . . . . . . . 11
⊢ ∅ ⊆ B |
26 | 25 | a1i 10 |
. . . . . . . . . 10
⊢ (¬ x ∈ dom F → ∅ ⊆ B) |
27 | 24, 26 | eqsstrd 3305 |
. . . . . . . . 9
⊢ (¬ x ∈ dom F → (F
‘x) ⊆ B) |
28 | 23, 27 | pm2.61i 156 |
. . . . . . . 8
⊢ (F ‘x)
⊆ B |
29 | | rsp 2674 |
. . . . . . . . 9
⊢ (∀x ∈ A B ⊆ C → (x
∈ A
→ B ⊆ C)) |
30 | 29 | impcom 419 |
. . . . . . . 8
⊢ ((x ∈ A ∧ ∀x ∈ A B ⊆ C) → B
⊆ C) |
31 | 28, 30 | syl5ss 3283 |
. . . . . . 7
⊢ ((x ∈ A ∧ ∀x ∈ A B ⊆ C) → (F
‘x) ⊆ C) |
32 | 31 | ex 423 |
. . . . . 6
⊢ (x ∈ A → (∀x ∈ A B ⊆ C → (F
‘x) ⊆ C)) |
33 | 7, 14, 17, 32 | vtoclgaf 2919 |
. . . . 5
⊢ (y ∈ A → (∀x ∈ A B ⊆ C → (F
‘y) ⊆ C)) |
34 | 6, 33 | vtoclga 2920 |
. . . 4
⊢ (D ∈ A → (∀x ∈ A B ⊆ C → (F
‘D) ⊆ C)) |
35 | 34 | impcom 419 |
. . 3
⊢ ((∀x ∈ A B ⊆ C ∧ D ∈ A) → (F
‘D) ⊆ C) |
36 | 3, 35 | sylan2 460 |
. 2
⊢ ((∀x ∈ A B ⊆ C ∧ D ∈ dom F) → (F
‘D) ⊆ C) |
37 | | ndmfv 5349 |
. . . 4
⊢ (¬ D ∈ dom F → (F
‘D) = ∅) |
38 | 37 | adantl 452 |
. . 3
⊢ ((∀x ∈ A B ⊆ C ∧ ¬ D ∈ dom F) → (F
‘D) = ∅) |
39 | | 0ss 3579 |
. . . 4
⊢ ∅ ⊆ C |
40 | 39 | a1i 10 |
. . 3
⊢ ((∀x ∈ A B ⊆ C ∧ ¬ D ∈ dom F) → ∅ ⊆ C) |
41 | 38, 40 | eqsstrd 3305 |
. 2
⊢ ((∀x ∈ A B ⊆ C ∧ ¬ D ∈ dom F) → (F
‘D) ⊆ C) |
42 | 36, 41 | pm2.61dan 766 |
1
⊢ (∀x ∈ A B ⊆ C → (F
‘D) ⊆ C) |