Step | Hyp | Ref
| Expression |
1 | | snssi 4339 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → {𝐴} ⊆ 𝑋) |
2 | 1 | adantl 482 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → {𝐴} ⊆ 𝑋) |
3 | | snnzg 4308 |
. . . 4
⊢ (𝐴 ∈ 𝑋 → {𝐴} ≠ ∅) |
4 | 3 | adantl 482 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → {𝐴} ≠ ∅) |
5 | | simpl 473 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → 𝑋 ∈ 𝑉) |
6 | | snfbas 21670 |
. . 3
⊢ (({𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅ ∧ 𝑋 ∈ 𝑉) → {{𝐴}} ∈ (fBas‘𝑋)) |
7 | 2, 4, 5, 6 | syl3anc 1326 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → {{𝐴}} ∈ (fBas‘𝑋)) |
8 | | selpw 4165 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋) |
9 | 8 | a1i 11 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋)) |
10 | | snex 4908 |
. . . . . . . 8
⊢ {𝐴} ∈ V |
11 | 10 | snid 4208 |
. . . . . . 7
⊢ {𝐴} ∈ {{𝐴}} |
12 | | snssi 4339 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑦 → {𝐴} ⊆ 𝑦) |
13 | | sseq1 3626 |
. . . . . . . 8
⊢ (𝑥 = {𝐴} → (𝑥 ⊆ 𝑦 ↔ {𝐴} ⊆ 𝑦)) |
14 | 13 | rspcev 3309 |
. . . . . . 7
⊢ (({𝐴} ∈ {{𝐴}} ∧ {𝐴} ⊆ 𝑦) → ∃𝑥 ∈ {{𝐴}}𝑥 ⊆ 𝑦) |
15 | 11, 12, 14 | sylancr 695 |
. . . . . 6
⊢ (𝐴 ∈ 𝑦 → ∃𝑥 ∈ {{𝐴}}𝑥 ⊆ 𝑦) |
16 | | intss1 4492 |
. . . . . . . . 9
⊢ (𝑥 ∈ {{𝐴}} → ∩
{{𝐴}} ⊆ 𝑥) |
17 | | sstr2 3610 |
. . . . . . . . 9
⊢ (∩ {{𝐴}} ⊆ 𝑥 → (𝑥 ⊆ 𝑦 → ∩ {{𝐴}} ⊆ 𝑦)) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ {{𝐴}} → (𝑥 ⊆ 𝑦 → ∩ {{𝐴}} ⊆ 𝑦)) |
19 | | snidg 4206 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴}) |
20 | 19 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ {𝐴}) |
21 | 10 | intsn 4513 |
. . . . . . . . . 10
⊢ ∩ {{𝐴}} = {𝐴} |
22 | 20, 21 | syl6eleqr 2712 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ ∩ {{𝐴}}) |
23 | | ssel 3597 |
. . . . . . . . 9
⊢ (∩ {{𝐴}} ⊆ 𝑦 → (𝐴 ∈ ∩ {{𝐴}} → 𝐴 ∈ 𝑦)) |
24 | 22, 23 | syl5com 31 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (∩
{{𝐴}} ⊆ 𝑦 → 𝐴 ∈ 𝑦)) |
25 | 18, 24 | sylan9r 690 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) ∧ 𝑥 ∈ {{𝐴}}) → (𝑥 ⊆ 𝑦 → 𝐴 ∈ 𝑦)) |
26 | 25 | rexlimdva 3031 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (∃𝑥 ∈ {{𝐴}}𝑥 ⊆ 𝑦 → 𝐴 ∈ 𝑦)) |
27 | 15, 26 | impbid2 216 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑦 ↔ ∃𝑥 ∈ {{𝐴}}𝑥 ⊆ 𝑦)) |
28 | 9, 27 | anbi12d 747 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → ((𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦) ↔ (𝑦 ⊆ 𝑋 ∧ ∃𝑥 ∈ {{𝐴}}𝑥 ⊆ 𝑦))) |
29 | | eleq2 2690 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
30 | 29 | elrab 3363 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} ↔ (𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦)) |
31 | 30 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} ↔ (𝑦 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑦))) |
32 | | elfg 21675 |
. . . . 5
⊢ ({{𝐴}} ∈ (fBas‘𝑋) → (𝑦 ∈ (𝑋filGen{{𝐴}}) ↔ (𝑦 ⊆ 𝑋 ∧ ∃𝑥 ∈ {{𝐴}}𝑥 ⊆ 𝑦))) |
33 | 7, 32 | syl 17 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (𝑦 ∈ (𝑋filGen{{𝐴}}) ↔ (𝑦 ⊆ 𝑋 ∧ ∃𝑥 ∈ {{𝐴}}𝑥 ⊆ 𝑦))) |
34 | 28, 31, 33 | 3bitr4d 300 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} ↔ 𝑦 ∈ (𝑋filGen{{𝐴}}))) |
35 | 34 | eqrdv 2620 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} = (𝑋filGen{{𝐴}})) |
36 | 7, 35 | jca 554 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → ({{𝐴}} ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} = (𝑋filGen{{𝐴}}))) |