Metamath Proof Explorer


Theorem baspartn

Description: A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion baspartn P V x P y P x = y x y = P TopBases

Proof

Step Hyp Ref Expression
1 id x P x P
2 pwidg x P x 𝒫 x
3 1 2 elind x P x P 𝒫 x
4 elssuni x P 𝒫 x x P 𝒫 x
5 3 4 syl x P x P 𝒫 x
6 inidm x x = x
7 ineq2 x = y x x = x y
8 6 7 eqtr3id x = y x = x y
9 8 pweqd x = y 𝒫 x = 𝒫 x y
10 9 ineq2d x = y P 𝒫 x = P 𝒫 x y
11 10 unieqd x = y P 𝒫 x = P 𝒫 x y
12 8 11 sseq12d x = y x P 𝒫 x x y P 𝒫 x y
13 5 12 syl5ibcom x P x = y x y P 𝒫 x y
14 0ss P 𝒫 x y
15 sseq1 x y = x y P 𝒫 x y P 𝒫 x y
16 14 15 mpbiri x y = x y P 𝒫 x y
17 16 a1i x P x y = x y P 𝒫 x y
18 13 17 jaod x P x = y x y = x y P 𝒫 x y
19 18 ralimdv x P y P x = y x y = y P x y P 𝒫 x y
20 19 ralimia x P y P x = y x y = x P y P x y P 𝒫 x y
21 20 adantl P V x P y P x = y x y = x P y P x y P 𝒫 x y
22 isbasisg P V P TopBases x P y P x y P 𝒫 x y
23 22 adantr P V x P y P x = y x y = P TopBases x P y P x y P 𝒫 x y
24 21 23 mpbird P V x P y P x = y x y = P TopBases