| Step | Hyp | Ref
| Expression |
| 1 | | fbasne0 23838 |
. . . . . 6
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) →
(fi‘𝐴) ≠
∅) |
| 2 | | fvprc 6898 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V →
(fi‘𝐴) =
∅) |
| 3 | 2 | necon1ai 2968 |
. . . . . 6
⊢
((fi‘𝐴) ≠
∅ → 𝐴 ∈
V) |
| 4 | 1, 3 | syl 17 |
. . . . 5
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) → 𝐴 ∈ V) |
| 5 | | ssfii 9459 |
. . . . 5
⊢ (𝐴 ∈ V → 𝐴 ⊆ (fi‘𝐴)) |
| 6 | 4, 5 | syl 17 |
. . . 4
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) → 𝐴 ⊆ (fi‘𝐴)) |
| 7 | | fbsspw 23840 |
. . . 4
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) →
(fi‘𝐴) ⊆
𝒫 𝑋) |
| 8 | 6, 7 | sstrd 3994 |
. . 3
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) → 𝐴 ⊆ 𝒫 𝑋) |
| 9 | | fieq0 9461 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝐴 = ∅ ↔
(fi‘𝐴) =
∅)) |
| 10 | 9 | necon3bid 2985 |
. . . . 5
⊢ (𝐴 ∈ V → (𝐴 ≠ ∅ ↔
(fi‘𝐴) ≠
∅)) |
| 11 | 10 | biimpar 477 |
. . . 4
⊢ ((𝐴 ∈ V ∧ (fi‘𝐴) ≠ ∅) → 𝐴 ≠ ∅) |
| 12 | 4, 1, 11 | syl2anc 584 |
. . 3
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) → 𝐴 ≠ ∅) |
| 13 | | 0nelfb 23839 |
. . 3
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) → ¬
∅ ∈ (fi‘𝐴)) |
| 14 | 8, 12, 13 | 3jca 1129 |
. 2
⊢
((fi‘𝐴) ∈
(fBas‘𝑋) →
(𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) |
| 15 | | simpr1 1195 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) → 𝐴 ⊆ 𝒫 𝑋) |
| 16 | | fipwss 9469 |
. . . . 5
⊢ (𝐴 ⊆ 𝒫 𝑋 → (fi‘𝐴) ⊆ 𝒫 𝑋) |
| 17 | 15, 16 | syl 17 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
(fi‘𝐴) ⊆
𝒫 𝑋) |
| 18 | | pwexg 5378 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V) |
| 19 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
𝒫 𝑋 ∈
V) |
| 20 | 19, 15 | ssexd 5324 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) → 𝐴 ∈ V) |
| 21 | | simpr2 1196 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) → 𝐴 ≠ ∅) |
| 22 | 10 | biimpa 476 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐴 ≠ ∅) →
(fi‘𝐴) ≠
∅) |
| 23 | 20, 21, 22 | syl2anc 584 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
(fi‘𝐴) ≠
∅) |
| 24 | | simpr3 1197 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) → ¬
∅ ∈ (fi‘𝐴)) |
| 25 | | df-nel 3047 |
. . . . . 6
⊢ (∅
∉ (fi‘𝐴) ↔
¬ ∅ ∈ (fi‘𝐴)) |
| 26 | 24, 25 | sylibr 234 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
∅ ∉ (fi‘𝐴)) |
| 27 | | fiin 9462 |
. . . . . . . 8
⊢ ((𝑥 ∈ (fi‘𝐴) ∧ 𝑦 ∈ (fi‘𝐴)) → (𝑥 ∩ 𝑦) ∈ (fi‘𝐴)) |
| 28 | | ssid 4006 |
. . . . . . . 8
⊢ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦) |
| 29 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑧 = (𝑥 ∩ 𝑦) → (𝑧 ⊆ (𝑥 ∩ 𝑦) ↔ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦))) |
| 30 | 29 | rspcev 3622 |
. . . . . . . 8
⊢ (((𝑥 ∩ 𝑦) ∈ (fi‘𝐴) ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦)) → ∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦)) |
| 31 | 27, 28, 30 | sylancl 586 |
. . . . . . 7
⊢ ((𝑥 ∈ (fi‘𝐴) ∧ 𝑦 ∈ (fi‘𝐴)) → ∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦)) |
| 32 | 31 | rgen2 3199 |
. . . . . 6
⊢
∀𝑥 ∈
(fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦) |
| 33 | 32 | a1i 11 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
∀𝑥 ∈
(fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦)) |
| 34 | 23, 26, 33 | 3jca 1129 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
((fi‘𝐴) ≠ ∅
∧ ∅ ∉ (fi‘𝐴) ∧ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)∃𝑧 ∈ (fi‘𝐴)𝑧 ⊆ (𝑥 ∩ 𝑦))) |
| 35 | | isfbas2 23843 |
. . . . 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 713 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴))) →
(fi‘𝐴) ∈
(fBas‘𝑋)) |
| 38 | 37 | ex 412 |
. 2
⊢ (𝑋 ∈ 𝑉 → ((𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴)) →
(fi‘𝐴) ∈
(fBas‘𝑋))) |
| 39 | 14, 38 | impbid2 226 |
1
⊢ (𝑋 ∈ 𝑉 → ((fi‘𝐴) ∈ (fBas‘𝑋) ↔ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈
(fi‘𝐴)))) |