Step | Hyp | Ref
| Expression |
1 | | elex 2723 |
. . 3
⊢ (𝐴 ∈ (fi‘𝐵) → 𝐴 ∈ V) |
2 | 1 | a1i 9 |
. 2
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) → 𝐴 ∈ V)) |
3 | | simpr 109 |
. . . . 5
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ 𝐴 = ∩ 𝑥) |
4 | | eldifsni 3689 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
→ 𝑥 ≠
∅) |
5 | 4 | adantr 274 |
. . . . . . 7
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ 𝑥 ≠
∅) |
6 | | eldifi 3229 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
→ 𝑥 ∈ (𝒫
𝐵 ∩
Fin)) |
7 | 6 | elin2d 3297 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
→ 𝑥 ∈
Fin) |
8 | 7 | adantr 274 |
. . . . . . . 8
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ 𝑥 ∈
Fin) |
9 | | fin0 6831 |
. . . . . . . 8
⊢ (𝑥 ∈ Fin → (𝑥 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝑥)) |
10 | 8, 9 | syl 14 |
. . . . . . 7
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ (𝑥 ≠ ∅
↔ ∃𝑧 𝑧 ∈ 𝑥)) |
11 | 5, 10 | mpbid 146 |
. . . . . 6
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ ∃𝑧 𝑧 ∈ 𝑥) |
12 | | inteximm 4111 |
. . . . . 6
⊢
(∃𝑧 𝑧 ∈ 𝑥 → ∩ 𝑥 ∈ V) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ ∩ 𝑥 ∈ V) |
14 | 3, 13 | eqeltrd 2234 |
. . . 4
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ 𝐴 ∈
V) |
15 | 14 | rexlimiva 2569 |
. . 3
⊢
(∃𝑥 ∈
((𝒫 𝐵 ∩ Fin)
∖ {∅})𝐴 = ∩ 𝑥
→ 𝐴 ∈
V) |
16 | 15 | a1i 9 |
. 2
⊢ (𝐵 ∈ 𝑉 → (∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥 → 𝐴 ∈ V)) |
17 | | elfi 6916 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥)) |
18 | | vprc 4097 |
. . . . . . . . . . 11
⊢ ¬ V
∈ V |
19 | | elsni 3578 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {∅} → 𝑥 = ∅) |
20 | 19 | inteqd 3813 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {∅} → ∩ 𝑥 =
∩ ∅) |
21 | | int0 3822 |
. . . . . . . . . . . . 13
⊢ ∩ ∅ = V |
22 | 20, 21 | eqtrdi 2206 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {∅} → ∩ 𝑥 =
V) |
23 | 22 | eleq1d 2226 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {∅} → (∩ 𝑥
∈ V ↔ V ∈ V)) |
24 | 18, 23 | mtbiri 665 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {∅} → ¬
∩ 𝑥 ∈ V) |
25 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → 𝐴 = ∩ 𝑥) |
26 | | simpll 519 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → 𝐴 ∈ V) |
27 | 25, 26 | eqeltrrd 2235 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → ∩ 𝑥
∈ V) |
28 | 24, 27 | nsyl3 616 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → ¬ 𝑥 ∈
{∅}) |
29 | 28 | biantrud 302 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ∧ ¬ 𝑥 ∈ {∅}))) |
30 | | eldif 3111 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
↔ (𝑥 ∈ (𝒫
𝐵 ∩ Fin) ∧ ¬
𝑥 ∈
{∅})) |
31 | 29, 30 | bitr4di 197 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↔ 𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖
{∅}))) |
32 | 31 | pm5.32da 448 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → ((𝐴 = ∩ 𝑥 ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) ↔ (𝐴 = ∩ 𝑥 ∧ 𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖
{∅})))) |
33 | | ancom 264 |
. . . . . 6
⊢ ((𝑥 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝐴 = ∩
𝑥) ↔ (𝐴 = ∩
𝑥 ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin))) |
34 | | ancom 264 |
. . . . . 6
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
↔ (𝐴 = ∩ 𝑥
∧ 𝑥 ∈ ((𝒫
𝐵 ∩ Fin) ∖
{∅}))) |
35 | 32, 33, 34 | 3bitr4g 222 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝐴 = ∩ 𝑥) ↔ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝐴 = ∩
𝑥))) |
36 | 35 | rexbidv2 2460 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥 ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖
{∅})𝐴 = ∩ 𝑥)) |
37 | 17, 36 | bitrd 187 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥)) |
38 | 37 | expcom 115 |
. 2
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ V → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥))) |
39 | 2, 16, 38 | pm5.21ndd 695 |
1
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥)) |