Metamath Proof Explorer


Theorem basis1

Description: Property of a basis. (Contributed by NM, 16-Jul-2006)

Ref Expression
Assertion basis1 B TopBases C B D B C D B 𝒫 C D

Proof

Step Hyp Ref Expression
1 isbasisg B TopBases B TopBases x B y B x y B 𝒫 x y
2 1 ibi B TopBases x B y B x y B 𝒫 x y
3 ineq1 x = C x y = C y
4 3 pweqd x = C 𝒫 x y = 𝒫 C y
5 4 ineq2d x = C B 𝒫 x y = B 𝒫 C y
6 5 unieqd x = C B 𝒫 x y = B 𝒫 C y
7 3 6 sseq12d x = C x y B 𝒫 x y C y B 𝒫 C y
8 ineq2 y = D C y = C D
9 8 pweqd y = D 𝒫 C y = 𝒫 C D
10 9 ineq2d y = D B 𝒫 C y = B 𝒫 C D
11 10 unieqd y = D B 𝒫 C y = B 𝒫 C D
12 8 11 sseq12d y = D C y B 𝒫 C y C D B 𝒫 C D
13 7 12 rspc2v C B D B x B y B x y B 𝒫 x y C D B 𝒫 C D
14 2 13 syl5com B TopBases C B D B C D B 𝒫 C D
15 14 3impib B TopBases C B D B C D B 𝒫 C D