Proof of Theorem elfi2
Step | Hyp | Ref
| Expression |
1 | | elex 3450 |
. . 3
⊢ (𝐴 ∈ (fi‘𝐵) → 𝐴 ∈ V) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) → 𝐴 ∈ V)) |
3 | | simpr 485 |
. . . . 5
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ 𝐴 = ∩ 𝑥) |
4 | | eldifsni 4723 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
→ 𝑥 ≠
∅) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ 𝑥 ≠
∅) |
6 | | intex 5261 |
. . . . . 6
⊢ (𝑥 ≠ ∅ ↔ ∩ 𝑥
∈ V) |
7 | 5, 6 | sylib 217 |
. . . . 5
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ ∩ 𝑥 ∈ V) |
8 | 3, 7 | eqeltrd 2839 |
. . . 4
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
→ 𝐴 ∈
V) |
9 | 8 | rexlimiva 3210 |
. . 3
⊢
(∃𝑥 ∈
((𝒫 𝐵 ∩ Fin)
∖ {∅})𝐴 = ∩ 𝑥
→ 𝐴 ∈
V) |
10 | 9 | a1i 11 |
. 2
⊢ (𝐵 ∈ 𝑉 → (∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥 → 𝐴 ∈ V)) |
11 | | elfi 9172 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥)) |
12 | | vprc 5239 |
. . . . . . . . . . 11
⊢ ¬ V
∈ V |
13 | | elsni 4578 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {∅} → 𝑥 = ∅) |
14 | 13 | inteqd 4884 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {∅} → ∩ 𝑥 =
∩ ∅) |
15 | | int0 4893 |
. . . . . . . . . . . . 13
⊢ ∩ ∅ = V |
16 | 14, 15 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {∅} → ∩ 𝑥 =
V) |
17 | 16 | eleq1d 2823 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {∅} → (∩ 𝑥
∈ V ↔ V ∈ V)) |
18 | 12, 17 | mtbiri 327 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {∅} → ¬
∩ 𝑥 ∈ V) |
19 | | simpr 485 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → 𝐴 = ∩ 𝑥) |
20 | | simpll 764 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → 𝐴 ∈ V) |
21 | 19, 20 | eqeltrrd 2840 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → ∩ 𝑥
∈ V) |
22 | 18, 21 | nsyl3 138 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → ¬ 𝑥 ∈
{∅}) |
23 | 22 | biantrud 532 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ∧ ¬ 𝑥 ∈ {∅}))) |
24 | | eldif 3897 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
↔ (𝑥 ∈ (𝒫
𝐵 ∩ Fin) ∧ ¬
𝑥 ∈
{∅})) |
25 | 23, 24 | bitr4di 289 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 = ∩ 𝑥) → (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↔ 𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖
{∅}))) |
26 | 25 | pm5.32da 579 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → ((𝐴 = ∩ 𝑥 ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) ↔ (𝐴 = ∩ 𝑥 ∧ 𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖
{∅})))) |
27 | | ancom 461 |
. . . . . 6
⊢ ((𝑥 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝐴 = ∩
𝑥) ↔ (𝐴 = ∩
𝑥 ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin))) |
28 | | ancom 461 |
. . . . . 6
⊢ ((𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝐴 = ∩ 𝑥)
↔ (𝐴 = ∩ 𝑥
∧ 𝑥 ∈ ((𝒫
𝐵 ∩ Fin) ∖
{∅}))) |
29 | 26, 27, 28 | 3bitr4g 314 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝐴 = ∩ 𝑥) ↔ (𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝐴 = ∩
𝑥))) |
30 | 29 | rexbidv2 3224 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥 ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖
{∅})𝐴 = ∩ 𝑥)) |
31 | 11, 30 | bitrd 278 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥)) |
32 | 31 | expcom 414 |
. 2
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ V → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥))) |
33 | 2, 10, 32 | pm5.21ndd 381 |
1
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩
𝑥)) |