Proof of Theorem elfi2
Step | Hyp | Ref
| Expression |
1 | | elex 3418 |
. . 3
⊢ (𝐴 ∈ (fi‘𝐵) → 𝐴 ∈ V) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) → 𝐴 ∈ V)) |
3 | | simpr 488 |
. . . . 5
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ 𝐴 = ∩ 𝑥) |
4 | | eldifsni 4688 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
→ 𝑥 ≠
∅) |
5 | 4 | adantr 484 |
. . . . . 6
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ 𝑥 ≠
∅) |
6 | | intex 5215 |
. . . . . 6
⊢ (𝑥 ≠ ∅ ↔ ∩ 𝑥
∈ V) |
7 | 5, 6 | sylib 221 |
. . . . 5
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ ∩ 𝑥 ∈ V) |
8 | 3, 7 | eqeltrd 2834 |
. . . 4
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ 𝐴 ∈
V) |
9 | 8 | rexlimiva 3192 |
. . 3
⊢
(∃𝑥 ∈
((𝒫 𝐵 ∩ Fin)
∖ {∅})𝐴 = ∩ 𝑥
→ 𝐴 ∈
V) |
10 | 9 | a1i 11 |
. 2
⊢ (𝐵 ∈ 𝑉 → (∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥 → 𝐴 ∈ V)) |
11 | | elfi 8962 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥)) |
12 | | vprc 5193 |
. . . . . . . . . . 11
⊢ ¬ V
∈ V |
13 | | elsni 4543 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {∅} → 𝑥 = ∅) |
14 | 13 | inteqd 4851 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {∅} → ∩ 𝑥 =
∩ ∅) |
15 | | int0 4860 |
. . . . . . . . . . . . 13
⊢ ∩ ∅ = V |
16 | 14, 15 | eqtrdi 2790 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {∅} → ∩ 𝑥 =
V) |
17 | 16 | eleq1d 2818 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {∅} → (∩ 𝑥
∈ V ↔ V ∈ V)) |
18 | 12, 17 | mtbiri 330 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {∅} → ¬
∩ 𝑥 ∈ V) |
19 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → 𝐴 = ∩ 𝑥) |
20 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → 𝐴 ∈ V) |
21 | 19, 20 | eqeltrrd 2835 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → ∩ 𝑥
∈ V) |
22 | 18, 21 | nsyl3 140 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → ¬ 𝑥 ∈
{∅}) |
23 | 22 | biantrud 535 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ∧ ¬ 𝑥 ∈ {∅}))) |
24 | | eldif 3863 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
↔ (𝑥 ∈ (𝒫
𝐵 ∩ Fin) ∧ ¬
𝑥 ∈
{∅})) |
25 | 23, 24 | bitr4di 292 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↔ 𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖
{∅}))) |
26 | 25 | pm5.32da 582 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → ((𝐴 = ∩ 𝑥 ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) ↔ (𝐴 = ∩ 𝑥 ∧ 𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖
{∅})))) |
27 | | ancom 464 |
. . . . . 6
⊢ ((𝑥 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝐴 = ∩
𝑥) ↔ (𝐴 = ∩
𝑥 ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin))) |
28 | | ancom 464 |
. . . . . 6
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
↔ (𝐴 = ∩ 𝑥
∧ 𝑥 ∈ ((𝒫
𝐵 ∩ Fin) ∖
{∅}))) |
29 | 26, 27, 28 | 3bitr4g 317 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝐴 = ∩ 𝑥) ↔ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝐴 = ∩
𝑥))) |
30 | 29 | rexbidv2 3206 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥 ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖
{∅})𝐴 = ∩ 𝑥)) |
31 | 11, 30 | bitrd 282 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥)) |
32 | 31 | expcom 417 |
. 2
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ V → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥))) |
33 | 2, 10, 32 | pm5.21ndd 384 |
1
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥)) |