| Step | Hyp | Ref
| Expression |
| 1 | | filfbas 23856 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) |
| 2 | | fbncp 23847 |
. . . . . . . 8
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐴 ∈ 𝐹) → ¬ (𝑋 ∖ 𝐴) ∈ 𝐹) |
| 3 | 1, 2 | sylan 580 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → ¬ (𝑋 ∖ 𝐴) ∈ 𝐹) |
| 4 | | filelss 23860 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ⊆ 𝑋) |
| 5 | | trfil3 23896 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝐹 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ (𝑋 ∖ 𝐴) ∈ 𝐹)) |
| 6 | 4, 5 | syldan 591 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → ((𝐹 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ (𝑋 ∖ 𝐴) ∈ 𝐹)) |
| 7 | 3, 6 | mpbird 257 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝐹 ↾t 𝐴) ∈ (Fil‘𝐴)) |
| 8 | | filfbas 23856 |
. . . . . 6
⊢ ((𝐹 ↾t 𝐴) ∈ (Fil‘𝐴) → (𝐹 ↾t 𝐴) ∈ (fBas‘𝐴)) |
| 9 | 7, 8 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝐹 ↾t 𝐴) ∈ (fBas‘𝐴)) |
| 10 | | restsspw 17476 |
. . . . . 6
⊢ (𝐹 ↾t 𝐴) ⊆ 𝒫 𝐴 |
| 11 | 4 | sspwd 4613 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝒫 𝐴 ⊆ 𝒫 𝑋) |
| 12 | 10, 11 | sstrid 3995 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝐹 ↾t 𝐴) ⊆ 𝒫 𝑋) |
| 13 | | filtop 23863 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
| 14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝑋 ∈ 𝐹) |
| 15 | | fbasweak 23873 |
. . . . 5
⊢ (((𝐹 ↾t 𝐴) ∈ (fBas‘𝐴) ∧ (𝐹 ↾t 𝐴) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐹) → (𝐹 ↾t 𝐴) ∈ (fBas‘𝑋)) |
| 16 | 9, 12, 14, 15 | syl3anc 1373 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝐹 ↾t 𝐴) ∈ (fBas‘𝑋)) |
| 17 | 1 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐹 ∈ (fBas‘𝑋)) |
| 18 | | trfilss 23897 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝐹 ↾t 𝐴) ⊆ 𝐹) |
| 19 | | fgss 23881 |
. . . 4
⊢ (((𝐹 ↾t 𝐴) ∈ (fBas‘𝑋) ∧ 𝐹 ∈ (fBas‘𝑋) ∧ (𝐹 ↾t 𝐴) ⊆ 𝐹) → (𝑋filGen(𝐹 ↾t 𝐴)) ⊆ (𝑋filGen𝐹)) |
| 20 | 16, 17, 18, 19 | syl3anc 1373 |
. . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑋filGen(𝐹 ↾t 𝐴)) ⊆ (𝑋filGen𝐹)) |
| 21 | | fgfil 23883 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹) |
| 22 | 21 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑋filGen𝐹) = 𝐹) |
| 23 | 20, 22 | sseqtrd 4020 |
. 2
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑋filGen(𝐹 ↾t 𝐴)) ⊆ 𝐹) |
| 24 | | filelss 23860 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐹) → 𝑥 ⊆ 𝑋) |
| 25 | 24 | ex 412 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐹 → 𝑥 ⊆ 𝑋)) |
| 26 | 25 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑥 ∈ 𝐹 → 𝑥 ⊆ 𝑋)) |
| 27 | | elrestr 17473 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝑥 ∈ 𝐹) → (𝑥 ∩ 𝐴) ∈ (𝐹 ↾t 𝐴)) |
| 28 | 27 | 3expa 1119 |
. . . . . . 7
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∩ 𝐴) ∈ (𝐹 ↾t 𝐴)) |
| 29 | | inss1 4237 |
. . . . . . 7
⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥 |
| 30 | | sseq1 4009 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 ∩ 𝐴) → (𝑦 ⊆ 𝑥 ↔ (𝑥 ∩ 𝐴) ⊆ 𝑥)) |
| 31 | 30 | rspcev 3622 |
. . . . . . 7
⊢ (((𝑥 ∩ 𝐴) ∈ (𝐹 ↾t 𝐴) ∧ (𝑥 ∩ 𝐴) ⊆ 𝑥) → ∃𝑦 ∈ (𝐹 ↾t 𝐴)𝑦 ⊆ 𝑥) |
| 32 | 28, 29, 31 | sylancl 586 |
. . . . . 6
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) ∧ 𝑥 ∈ 𝐹) → ∃𝑦 ∈ (𝐹 ↾t 𝐴)𝑦 ⊆ 𝑥) |
| 33 | 32 | ex 412 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑥 ∈ 𝐹 → ∃𝑦 ∈ (𝐹 ↾t 𝐴)𝑦 ⊆ 𝑥)) |
| 34 | 26, 33 | jcad 512 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑥 ∈ 𝐹 → (𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝐹 ↾t 𝐴)𝑦 ⊆ 𝑥))) |
| 35 | | elfg 23879 |
. . . . 5
⊢ ((𝐹 ↾t 𝐴) ∈ (fBas‘𝑋) → (𝑥 ∈ (𝑋filGen(𝐹 ↾t 𝐴)) ↔ (𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝐹 ↾t 𝐴)𝑦 ⊆ 𝑥))) |
| 36 | 16, 35 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑥 ∈ (𝑋filGen(𝐹 ↾t 𝐴)) ↔ (𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝐹 ↾t 𝐴)𝑦 ⊆ 𝑥))) |
| 37 | 34, 36 | sylibrd 259 |
. . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑥 ∈ 𝐹 → 𝑥 ∈ (𝑋filGen(𝐹 ↾t 𝐴)))) |
| 38 | 37 | ssrdv 3989 |
. 2
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐹 ⊆ (𝑋filGen(𝐹 ↾t 𝐴))) |
| 39 | 23, 38 | eqssd 4001 |
1
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑋filGen(𝐹 ↾t 𝐴)) = 𝐹) |