| Step | Hyp | Ref
| Expression |
| 1 | | simp3 1139 |
. 2
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → 𝐹 ⊆ 𝐺) |
| 2 | | filelss 23860 |
. . . . . 6
⊢ ((𝐺 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐺) → 𝑥 ⊆ 𝑋) |
| 3 | 2 | ex 412 |
. . . . 5
⊢ (𝐺 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐺 → 𝑥 ⊆ 𝑋)) |
| 4 | 3 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → (𝑥 ∈ 𝐺 → 𝑥 ⊆ 𝑋)) |
| 5 | | ufilb 23914 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 ↔ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
| 6 | 5 | 3ad2antl1 1186 |
. . . . . . . 8
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 ↔ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
| 7 | | simpl3 1194 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ 𝐺) |
| 8 | 7 | sseld 3982 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → (𝑋 ∖ 𝑥) ∈ 𝐺)) |
| 9 | | filfbas 23856 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ (Fil‘𝑋) → 𝐺 ∈ (fBas‘𝑋)) |
| 10 | | fbncp 23847 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ (fBas‘𝑋) ∧ 𝑥 ∈ 𝐺) → ¬ (𝑋 ∖ 𝑥) ∈ 𝐺) |
| 11 | 10 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ (fBas‘𝑋) → (𝑥 ∈ 𝐺 → ¬ (𝑋 ∖ 𝑥) ∈ 𝐺)) |
| 12 | 9, 11 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐺 → ¬ (𝑋 ∖ 𝑥) ∈ 𝐺)) |
| 13 | 12 | con2d 134 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ (Fil‘𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐺 → ¬ 𝑥 ∈ 𝐺)) |
| 14 | 13 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → ((𝑋 ∖ 𝑥) ∈ 𝐺 → ¬ 𝑥 ∈ 𝐺)) |
| 15 | 14 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐺 → ¬ 𝑥 ∈ 𝐺)) |
| 16 | 8, 15 | syld 47 |
. . . . . . . 8
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → ¬ 𝑥 ∈ 𝐺)) |
| 17 | 6, 16 | sylbid 240 |
. . . . . . 7
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ 𝐺)) |
| 18 | 17 | con4d 115 |
. . . . . 6
⊢ (((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐺 → 𝑥 ∈ 𝐹)) |
| 19 | 18 | ex 412 |
. . . . 5
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝐺 → 𝑥 ∈ 𝐹))) |
| 20 | 19 | com23 86 |
. . . 4
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → (𝑥 ∈ 𝐺 → (𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝐹))) |
| 21 | 4, 20 | mpdd 43 |
. . 3
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → (𝑥 ∈ 𝐺 → 𝑥 ∈ 𝐹)) |
| 22 | 21 | ssrdv 3989 |
. 2
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → 𝐺 ⊆ 𝐹) |
| 23 | 1, 22 | eqssd 4001 |
1
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → 𝐹 = 𝐺) |