Step | Hyp | Ref
| Expression |
1 | | elfvex 6131 |
. . . . . 6
⊢ (𝐴 ∈ (fi‘𝐶) → 𝐶 ∈ V) |
2 | | elfi 8202 |
. . . . . 6
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐶 ∈ V) → (𝐴 ∈ (fi‘𝐶) ↔ ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = ∩ 𝑥)) |
3 | 1, 2 | mpdan 699 |
. . . . 5
⊢ (𝐴 ∈ (fi‘𝐶) → (𝐴 ∈ (fi‘𝐶) ↔ ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = ∩ 𝑥)) |
4 | 3 | ibi 255 |
. . . 4
⊢ (𝐴 ∈ (fi‘𝐶) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = ∩ 𝑥) |
5 | 4 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)𝐴 = ∩ 𝑥) |
6 | | simpr 476 |
. . . 4
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → 𝐵 ∈ (fi‘𝐶)) |
7 | | elfi 8202 |
. . . . . 6
⊢ ((𝐵 ∈ (fi‘𝐶) ∧ 𝐶 ∈ V) → (𝐵 ∈ (fi‘𝐶) ↔ ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)𝐵 = ∩ 𝑦)) |
8 | 7 | ancoms 468 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ (fi‘𝐶)) → (𝐵 ∈ (fi‘𝐶) ↔ ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)𝐵 = ∩ 𝑦)) |
9 | 1, 8 | sylan 487 |
. . . 4
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → (𝐵 ∈ (fi‘𝐶) ↔ ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)𝐵 = ∩ 𝑦)) |
10 | 6, 9 | mpbid 221 |
. . 3
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)𝐵 = ∩ 𝑦) |
11 | | elin 3758 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝐶 ∧ 𝑥 ∈ Fin)) |
12 | | elin 3758 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑦 ∈ 𝒫 𝐶 ∧ 𝑦 ∈ Fin)) |
13 | | elpwi 4117 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 𝐶 → 𝑥 ⊆ 𝐶) |
14 | | elpwi 4117 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝒫 𝐶 → 𝑦 ⊆ 𝐶) |
15 | 13, 14 | anim12i 588 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝒫 𝐶 ∧ 𝑦 ∈ 𝒫 𝐶) → (𝑥 ⊆ 𝐶 ∧ 𝑦 ⊆ 𝐶)) |
16 | | unss 3749 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ 𝐶 ∧ 𝑦 ⊆ 𝐶) ↔ (𝑥 ∪ 𝑦) ⊆ 𝐶) |
17 | 15, 16 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 𝐶 ∧ 𝑦 ∈ 𝒫 𝐶) → (𝑥 ∪ 𝑦) ⊆ 𝐶) |
18 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
19 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
20 | 18, 19 | unex 6854 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∪ 𝑦) ∈ V |
21 | 20 | elpw 4114 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∪ 𝑦) ∈ 𝒫 𝐶 ↔ (𝑥 ∪ 𝑦) ⊆ 𝐶) |
22 | 17, 21 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 𝐶 ∧ 𝑦 ∈ 𝒫 𝐶) → (𝑥 ∪ 𝑦) ∈ 𝒫 𝐶) |
23 | | unfi 8112 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝑥 ∪ 𝑦) ∈ Fin) |
24 | 22, 23 | anim12i 588 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝒫 𝐶 ∧ 𝑦 ∈ 𝒫 𝐶) ∧ (𝑥 ∈ Fin ∧ 𝑦 ∈ Fin)) → ((𝑥 ∪ 𝑦) ∈ 𝒫 𝐶 ∧ (𝑥 ∪ 𝑦) ∈ Fin)) |
25 | 24 | an4s 865 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝒫 𝐶 ∧ 𝑥 ∈ Fin) ∧ (𝑦 ∈ 𝒫 𝐶 ∧ 𝑦 ∈ Fin)) → ((𝑥 ∪ 𝑦) ∈ 𝒫 𝐶 ∧ (𝑥 ∪ 𝑦) ∈ Fin)) |
26 | 11, 12, 25 | syl2anb 495 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝒫 𝐶 ∩ Fin) ∧ 𝑦 ∈ (𝒫 𝐶 ∩ Fin)) → ((𝑥 ∪ 𝑦) ∈ 𝒫 𝐶 ∧ (𝑥 ∪ 𝑦) ∈ Fin)) |
27 | | elin 3758 |
. . . . . . . 8
⊢ ((𝑥 ∪ 𝑦) ∈ (𝒫 𝐶 ∩ Fin) ↔ ((𝑥 ∪ 𝑦) ∈ 𝒫 𝐶 ∧ (𝑥 ∪ 𝑦) ∈ Fin)) |
28 | 26, 27 | sylibr 223 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝒫 𝐶 ∩ Fin) ∧ 𝑦 ∈ (𝒫 𝐶 ∩ Fin)) → (𝑥 ∪ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
29 | | ineq12 3771 |
. . . . . . . 8
⊢ ((𝐴 = ∩
𝑥 ∧ 𝐵 = ∩ 𝑦) → (𝐴 ∩ 𝐵) = (∩ 𝑥 ∩ ∩ 𝑦)) |
30 | | intun 4444 |
. . . . . . . 8
⊢ ∩ (𝑥
∪ 𝑦) = (∩ 𝑥
∩ ∩ 𝑦) |
31 | 29, 30 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝐴 = ∩
𝑥 ∧ 𝐵 = ∩ 𝑦) → (𝐴 ∩ 𝐵) = ∩ (𝑥 ∪ 𝑦)) |
32 | | inteq 4413 |
. . . . . . . . 9
⊢ (𝑧 = (𝑥 ∪ 𝑦) → ∩ 𝑧 = ∩
(𝑥 ∪ 𝑦)) |
33 | 32 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑧 = (𝑥 ∪ 𝑦) → ((𝐴 ∩ 𝐵) = ∩ 𝑧 ↔ (𝐴 ∩ 𝐵) = ∩ (𝑥 ∪ 𝑦))) |
34 | 33 | rspcev 3282 |
. . . . . . 7
⊢ (((𝑥 ∪ 𝑦) ∈ (𝒫 𝐶 ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∩ (𝑥 ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝐴 ∩ 𝐵) = ∩ 𝑧) |
35 | 28, 31, 34 | syl2an 493 |
. . . . . 6
⊢ (((𝑥 ∈ (𝒫 𝐶 ∩ Fin) ∧ 𝑦 ∈ (𝒫 𝐶 ∩ Fin)) ∧ (𝐴 = ∩
𝑥 ∧ 𝐵 = ∩ 𝑦)) → ∃𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝐴 ∩ 𝐵) = ∩ 𝑧) |
36 | 35 | an4s 865 |
. . . . 5
⊢ (((𝑥 ∈ (𝒫 𝐶 ∩ Fin) ∧ 𝐴 = ∩
𝑥) ∧ (𝑦 ∈ (𝒫 𝐶 ∩ Fin) ∧ 𝐵 = ∩
𝑦)) → ∃𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝐴 ∩ 𝐵) = ∩ 𝑧) |
37 | 36 | rexlimdvaa 3014 |
. . . 4
⊢ ((𝑥 ∈ (𝒫 𝐶 ∩ Fin) ∧ 𝐴 = ∩
𝑥) → (∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)𝐵 = ∩ 𝑦 → ∃𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝐴 ∩ 𝐵) = ∩ 𝑧)) |
38 | 37 | rexlimiva 3010 |
. . 3
⊢
(∃𝑥 ∈
(𝒫 𝐶 ∩
Fin)𝐴 = ∩ 𝑥
→ (∃𝑦 ∈
(𝒫 𝐶 ∩
Fin)𝐵 = ∩ 𝑦
→ ∃𝑧 ∈
(𝒫 𝐶 ∩
Fin)(𝐴 ∩ 𝐵) = ∩
𝑧)) |
39 | 5, 10, 38 | sylc 63 |
. 2
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → ∃𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝐴 ∩ 𝐵) = ∩ 𝑧) |
40 | | inex1g 4729 |
. . . 4
⊢ (𝐴 ∈ (fi‘𝐶) → (𝐴 ∩ 𝐵) ∈ V) |
41 | | elfi 8202 |
. . . 4
⊢ (((𝐴 ∩ 𝐵) ∈ V ∧ 𝐶 ∈ V) → ((𝐴 ∩ 𝐵) ∈ (fi‘𝐶) ↔ ∃𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝐴 ∩ 𝐵) = ∩ 𝑧)) |
42 | 40, 1, 41 | syl2anc 691 |
. . 3
⊢ (𝐴 ∈ (fi‘𝐶) → ((𝐴 ∩ 𝐵) ∈ (fi‘𝐶) ↔ ∃𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝐴 ∩ 𝐵) = ∩ 𝑧)) |
43 | 42 | adantr 480 |
. 2
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → ((𝐴 ∩ 𝐵) ∈ (fi‘𝐶) ↔ ∃𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝐴 ∩ 𝐵) = ∩ 𝑧)) |
44 | 39, 43 | mpbird 246 |
1
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → (𝐴 ∩ 𝐵) ∈ (fi‘𝐶)) |