Step | Hyp | Ref
| Expression |
1 | | imainlem 4923 |
. . 3
⊢ (𝐹 “ (A ∩ B))
⊆ ((𝐹 “
A) ∩ (𝐹 “ B)) |
2 | 1 | a1i 9 |
. 2
⊢ (Fun
◡𝐹 → (𝐹 “ (A ∩ B))
⊆ ((𝐹 “
A) ∩ (𝐹 “ B))) |
3 | | eeanv 1804 |
. . . . . 6
⊢ (∃x∃z((x ∈ A ∧ x𝐹y) ∧ (z ∈ B ∧ z𝐹y)) ↔ (∃x(x ∈ A ∧ x𝐹y) ∧ ∃z(z ∈ B ∧ z𝐹y))) |
4 | | simprll 489 |
. . . . . . . . . . 11
⊢ ((Fun
◡𝐹 ∧
((x ∈
A ∧
x𝐹y) ∧ (z ∈ B ∧ z𝐹y))) → x
∈ A) |
5 | | simpr 103 |
. . . . . . . . . . . . . 14
⊢
((x ∈ A ∧ x𝐹y) → x𝐹y) |
6 | | simpr 103 |
. . . . . . . . . . . . . 14
⊢
((z ∈ B ∧ z𝐹y) → z𝐹y) |
7 | 5, 6 | anim12i 321 |
. . . . . . . . . . . . 13
⊢
(((x ∈ A ∧ x𝐹y) ∧ (z ∈ B ∧ z𝐹y))
→ (x𝐹y ∧ z𝐹y)) |
8 | | funcnveq 4905 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
◡𝐹 ↔ ∀x∀y∀z((x𝐹y ∧ z𝐹y) → x =
z)) |
9 | 8 | biimpi 113 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
◡𝐹 → ∀x∀y∀z((x𝐹y ∧ z𝐹y) → x =
z)) |
10 | 9 | 19.21bi 1447 |
. . . . . . . . . . . . . . 15
⊢ (Fun
◡𝐹 → ∀y∀z((x𝐹y ∧ z𝐹y) → x =
z)) |
11 | 10 | 19.21bbi 1448 |
. . . . . . . . . . . . . 14
⊢ (Fun
◡𝐹 → ((x𝐹y ∧ z𝐹y) → x =
z)) |
12 | 11 | imp 115 |
. . . . . . . . . . . . 13
⊢ ((Fun
◡𝐹 ∧
(x𝐹y ∧ z𝐹y)) → x =
z) |
13 | 7, 12 | sylan2 270 |
. . . . . . . . . . . 12
⊢ ((Fun
◡𝐹 ∧
((x ∈
A ∧
x𝐹y) ∧ (z ∈ B ∧ z𝐹y))) → x =
z) |
14 | | simprrl 491 |
. . . . . . . . . . . 12
⊢ ((Fun
◡𝐹 ∧
((x ∈
A ∧
x𝐹y) ∧ (z ∈ B ∧ z𝐹y))) → z
∈ B) |
15 | 13, 14 | eqeltrd 2111 |
. . . . . . . . . . 11
⊢ ((Fun
◡𝐹 ∧
((x ∈
A ∧
x𝐹y) ∧ (z ∈ B ∧ z𝐹y))) → x
∈ B) |
16 | | elin 3120 |
. . . . . . . . . . 11
⊢ (x ∈ (A ∩ B)
↔ (x ∈ A ∧ x ∈ B)) |
17 | 4, 15, 16 | sylanbrc 394 |
. . . . . . . . . 10
⊢ ((Fun
◡𝐹 ∧
((x ∈
A ∧
x𝐹y) ∧ (z ∈ B ∧ z𝐹y))) → x
∈ (A
∩ B)) |
18 | | simprlr 490 |
. . . . . . . . . 10
⊢ ((Fun
◡𝐹 ∧
((x ∈
A ∧
x𝐹y) ∧ (z ∈ B ∧ z𝐹y))) → x𝐹y) |
19 | 17, 18 | jca 290 |
. . . . . . . . 9
⊢ ((Fun
◡𝐹 ∧
((x ∈
A ∧
x𝐹y) ∧ (z ∈ B ∧ z𝐹y))) → (x
∈ (A
∩ B) ∧
x𝐹y)) |
20 | 19 | ex 108 |
. . . . . . . 8
⊢ (Fun
◡𝐹 → (((x ∈ A ∧ x𝐹y) ∧ (z ∈ B ∧ z𝐹y)) → (x
∈ (A
∩ B) ∧
x𝐹y))) |
21 | 20 | exlimdv 1697 |
. . . . . . 7
⊢ (Fun
◡𝐹 → (∃z((x ∈ A ∧ x𝐹y) ∧ (z ∈ B ∧ z𝐹y)) → (x
∈ (A
∩ B) ∧
x𝐹y))) |
22 | 21 | eximdv 1757 |
. . . . . 6
⊢ (Fun
◡𝐹 → (∃x∃z((x ∈ A ∧ x𝐹y) ∧ (z ∈ B ∧ z𝐹y)) → ∃x(x ∈ (A ∩ B) ∧ x𝐹y))) |
23 | 3, 22 | syl5bir 142 |
. . . . 5
⊢ (Fun
◡𝐹 → ((∃x(x ∈ A ∧ x𝐹y) ∧ ∃z(z ∈ B ∧ z𝐹y)) → ∃x(x ∈ (A ∩ B) ∧ x𝐹y))) |
24 | | df-rex 2306 |
. . . . . 6
⊢ (∃x ∈ A x𝐹y ↔
∃x(x ∈ A ∧ x𝐹y)) |
25 | | df-rex 2306 |
. . . . . 6
⊢ (∃z ∈ B z𝐹y ↔
∃z(z ∈ B ∧ z𝐹y)) |
26 | 24, 25 | anbi12i 433 |
. . . . 5
⊢ ((∃x ∈ A x𝐹y ∧ ∃z ∈ B z𝐹y) ↔ (∃x(x ∈ A ∧ x𝐹y) ∧ ∃z(z ∈ B ∧ z𝐹y))) |
27 | | df-rex 2306 |
. . . . 5
⊢ (∃x ∈ (A ∩
B)x𝐹y ↔
∃x(x ∈ (A ∩
B) ∧
x𝐹y)) |
28 | 23, 26, 27 | 3imtr4g 194 |
. . . 4
⊢ (Fun
◡𝐹 → ((∃x ∈ A x𝐹y ∧ ∃z ∈ B z𝐹y) → ∃x ∈ (A ∩
B)x𝐹y)) |
29 | 28 | ss2abdv 3007 |
. . 3
⊢ (Fun
◡𝐹 → {y ∣ (∃x ∈ A x𝐹y ∧ ∃z ∈ B z𝐹y)} ⊆ {y
∣ ∃x ∈ (A ∩ B)x𝐹y}) |
30 | | dfima2 4613 |
. . . . 5
⊢ (𝐹 “ A) = {y ∣
∃x ∈ A x𝐹y} |
31 | | dfima2 4613 |
. . . . 5
⊢ (𝐹 “ B) = {y ∣
∃z ∈ B z𝐹y} |
32 | 30, 31 | ineq12i 3130 |
. . . 4
⊢ ((𝐹 “ A) ∩ (𝐹 “ B)) = ({y
∣ ∃x ∈ A x𝐹y} ∩ {y
∣ ∃z ∈ B z𝐹y}) |
33 | | inab 3199 |
. . . 4
⊢
({y ∣ ∃x ∈ A x𝐹y} ∩
{y ∣ ∃z ∈ B z𝐹y}) =
{y ∣ (∃x ∈ A x𝐹y ∧ ∃z ∈ B z𝐹y)} |
34 | 32, 33 | eqtri 2057 |
. . 3
⊢ ((𝐹 “ A) ∩ (𝐹 “ B)) = {y ∣
(∃x
∈ A
x𝐹y ∧ ∃z ∈ B z𝐹y)} |
35 | | dfima2 4613 |
. . 3
⊢ (𝐹 “ (A ∩ B)) =
{y ∣ ∃x ∈ (A ∩
B)x𝐹y} |
36 | 29, 34, 35 | 3sstr4g 2980 |
. 2
⊢ (Fun
◡𝐹 → ((𝐹 “ A) ∩ (𝐹 “ B)) ⊆ (𝐹 “ (A ∩ B))) |
37 | 2, 36 | eqssd 2956 |
1
⊢ (Fun
◡𝐹 → (𝐹 “ (A ∩ B)) =
((𝐹 “ A) ∩ (𝐹 “ B))) |