Step | Hyp | Ref
| Expression |
1 | | fbasne0 21444 |
. . . . . 6
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) →
(fi‘𝐴) ≠
∅) |
2 | | fvprc 6097 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V →
(fi‘𝐴) =
∅) |
3 | 2 | necon1ai 2809 |
. . . . . 6
⊢
((fi‘𝐴) ≠
∅ → 𝐴 ∈
V) |
4 | 1, 3 | syl 17 |
. . . . 5
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) → 𝐴 ∈ V) |
5 | | ssfii 8208 |
. . . . 5
⊢ (𝐴 ∈ V → 𝐴 ⊆ (fi‘𝐴)) |
6 | 4, 5 | syl 17 |
. . . 4
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) → 𝐴 ⊆ (fi‘𝐴)) |
7 | | fbsspw 21446 |
. . . 4
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) →
(fi‘𝐴) ⊆
𝒫 𝑋) |
8 | 6, 7 | sstrd 3578 |
. . 3
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) → 𝐴 ⊆ 𝒫 𝑋) |
9 | | fieq0 8210 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝐴 = ∅ ↔
(fi‘𝐴) =
∅)) |
10 | 9 | necon3bid 2826 |
. . . . 5
⊢ (𝐴 ∈ V → (𝐴 ≠ ∅ ↔
(fi‘𝐴) ≠
∅)) |
11 | 10 | biimpar 501 |
. . . 4
⊢ ((𝐴 ∈ V ∧ (fi‘𝐴) ≠ ∅) → 𝐴 ≠ ∅) |
12 | 4, 1, 11 | syl2anc 691 |
. . 3
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) → 𝐴 ≠ ∅) |
13 | | 0nelfb 21445 |
. . 3
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) → ¬
∅ ∈ (fi‘𝐴)) |
14 | 8, 12, 13 | 3jca 1235 |
. 2
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) →
(𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) |
15 | | simpr1 1060 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) → 𝐴 ⊆ 𝒫 𝑋) |
16 | | fipwss 8218 |
. . . . 5
⊢ (𝐴 ⊆ 𝒫 𝑋 → (fi‘𝐴) ⊆ 𝒫 𝑋) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
(fi‘𝐴) ⊆
𝒫 𝑋) |
18 | | pwexg 4776 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V) |
19 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
𝒫 𝑋 ∈
V) |
20 | 19, 15 | ssexd 4733 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) → 𝐴 ∈ V) |
21 | | simpr2 1061 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) → 𝐴 ≠ ∅) |
22 | 10 | biimpa 500 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐴 ≠ ∅) →
(fi‘𝐴) ≠
∅) |
23 | 20, 21, 22 | syl2anc 691 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
(fi‘𝐴) ≠
∅) |
24 | | simpr3 1062 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) → ¬
∅ ∈ (fi‘𝐴)) |
25 | | df-nel 2783 |
. . . . . 6
⊢ (∅
∉ (fi‘𝐴) ↔
¬ ∅ ∈ (fi‘𝐴)) |
26 | 24, 25 | sylibr 223 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
∅ ∉ (fi‘𝐴)) |
27 | | fiin 8211 |
. . . . . . . 8
⊢ ((𝑥 ∈ (fi‘𝐴) ∧ 𝑦 ∈ (fi‘𝐴)) → (𝑥 ∩ 𝑦) ∈ (fi‘𝐴)) |
28 | | ssid 3587 |
. . . . . . . 8
⊢ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦) |
29 | | sseq1 3589 |
. . . . . . . . 9
⊢ (𝑧 = (𝑥 ∩ 𝑦) → (𝑧 ⊆ (𝑥 ∩ 𝑦) ↔ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦))) |
30 | 29 | rspcev 3282 |
. . . . . . . 8
⊢ (((𝑥 ∩ 𝑦) ∈ (fi‘𝐴) ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦)) → ∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦)) |
31 | 27, 28, 30 | sylancl 693 |
. . . . . . 7
⊢ ((𝑥 ∈ (fi‘𝐴) ∧ 𝑦 ∈ (fi‘𝐴)) → ∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦)) |
32 | 31 | rgen2a 2960 |
. . . . . 6
⊢
∀𝑥 ∈
(fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦) |
33 | 32 | a1i 11 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
∀𝑥 ∈
(fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦)) |
34 | 23, 26, 33 | 3jca 1235 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
((fi‘𝐴) ≠ ∅
∧ ∅ ∉ (fi‘𝐴) ∧ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦))) |
35 | | isfbas2 21449 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → ((fi‘𝐴) ∈ (fBas‘𝑋) ↔ ((fi‘𝐴) ⊆ 𝒫 𝑋 ∧ ((fi‘𝐴) ≠ ∅ ∧ ∅ ∉
(fi‘𝐴) ∧
∀𝑥 ∈
(fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
36 | 35 | adantr 480 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
((fi‘𝐴) ∈
(fBas‘𝑋) ↔
((fi‘𝐴) ⊆
𝒫 𝑋 ∧
((fi‘𝐴) ≠ ∅
∧ ∅ ∉ (fi‘𝐴) ∧ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
37 | 17, 34, 36 | mpbir2and 959 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
(fi‘𝐴) ∈
(fBas‘𝑋)) |
38 | 37 | ex 449 |
. 2
⊢ (𝑋 ∈ 𝑉 → ((𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴)) →
(fi‘𝐴) ∈
(fBas‘𝑋))) |
39 | 14, 38 | impbid2 215 |
1
⊢ (𝑋 ∈ 𝑉 → ((fi‘𝐴) ∈ (fBas‘𝑋) ↔ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴)))) |