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 e. V /\ A. x e. P A. y e. P ( x = y \/ ( x i^i y ) = (/) ) ) -> P e. TopBases )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( x e. P -> x e. P )
2 pwidg 
 |-  ( x e. P -> x e. ~P x )
3 1 2 elind 
 |-  ( x e. P -> x e. ( P i^i ~P x ) )
4 elssuni 
 |-  ( x e. ( P i^i ~P x ) -> x C_ U. ( P i^i ~P x ) )
5 3 4 syl 
 |-  ( x e. P -> x C_ U. ( P i^i ~P x ) )
6 inidm 
 |-  ( x i^i x ) = x
7 ineq2 
 |-  ( x = y -> ( x i^i x ) = ( x i^i y ) )
8 6 7 eqtr3id 
 |-  ( x = y -> x = ( x i^i y ) )
9 8 pweqd 
 |-  ( x = y -> ~P x = ~P ( x i^i y ) )
10 9 ineq2d 
 |-  ( x = y -> ( P i^i ~P x ) = ( P i^i ~P ( x i^i y ) ) )
11 10 unieqd 
 |-  ( x = y -> U. ( P i^i ~P x ) = U. ( P i^i ~P ( x i^i y ) ) )
12 8 11 sseq12d 
 |-  ( x = y -> ( x C_ U. ( P i^i ~P x ) <-> ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) ) )
13 5 12 syl5ibcom 
 |-  ( x e. P -> ( x = y -> ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) ) )
14 0ss 
 |-  (/) C_ U. ( P i^i ~P ( x i^i y ) )
15 sseq1 
 |-  ( ( x i^i y ) = (/) -> ( ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) <-> (/) C_ U. ( P i^i ~P ( x i^i y ) ) ) )
16 14 15 mpbiri 
 |-  ( ( x i^i y ) = (/) -> ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) )
17 16 a1i 
 |-  ( x e. P -> ( ( x i^i y ) = (/) -> ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) ) )
18 13 17 jaod 
 |-  ( x e. P -> ( ( x = y \/ ( x i^i y ) = (/) ) -> ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) ) )
19 18 ralimdv 
 |-  ( x e. P -> ( A. y e. P ( x = y \/ ( x i^i y ) = (/) ) -> A. y e. P ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) ) )
20 19 ralimia 
 |-  ( A. x e. P A. y e. P ( x = y \/ ( x i^i y ) = (/) ) -> A. x e. P A. y e. P ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) )
21 20 adantl 
 |-  ( ( P e. V /\ A. x e. P A. y e. P ( x = y \/ ( x i^i y ) = (/) ) ) -> A. x e. P A. y e. P ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) )
22 isbasisg 
 |-  ( P e. V -> ( P e. TopBases <-> A. x e. P A. y e. P ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) ) )
23 22 adantr 
 |-  ( ( P e. V /\ A. x e. P A. y e. P ( x = y \/ ( x i^i y ) = (/) ) ) -> ( P e. TopBases <-> A. x e. P A. y e. P ( x i^i y ) C_ U. ( P i^i ~P ( x i^i y ) ) ) )
24 21 23 mpbird 
 |-  ( ( P e. V /\ A. x e. P A. y e. P ( x = y \/ ( x i^i y ) = (/) ) ) -> P e. TopBases )