Metamath Proof Explorer

Theorem basdif0

Description: A basis is not affected by the addition or removal of the empty set. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Assertion basdif0 
|- ( ( B \ { (/) } ) e. TopBases <-> B e. TopBases )

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  B C_ ( B u. { (/) } )
2 undif1 
 |-  ( ( B \ { (/) } ) u. { (/) } ) = ( B u. { (/) } )
3 1 2 sseqtrri 
 |-  B C_ ( ( B \ { (/) } ) u. { (/) } )
4 snex 
 |-  { (/) } e. _V
5 unexg 
 |-  ( ( ( B \ { (/) } ) e. TopBases /\ { (/) } e. _V ) -> ( ( B \ { (/) } ) u. { (/) } ) e. _V )
6 4 5 mpan2 
 |-  ( ( B \ { (/) } ) e. TopBases -> ( ( B \ { (/) } ) u. { (/) } ) e. _V )
7 ssexg 
 |-  ( ( B C_ ( ( B \ { (/) } ) u. { (/) } ) /\ ( ( B \ { (/) } ) u. { (/) } ) e. _V ) -> B e. _V )
8 3 6 7 sylancr 
 |-  ( ( B \ { (/) } ) e. TopBases -> B e. _V )
9 elex 
 |-  ( B e. TopBases -> B e. _V )
10 indif1 
 |-  ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) = ( ( B i^i ~P ( x i^i y ) ) \ { (/) } )
11 10 unieqi 
 |-  U. ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) = U. ( ( B i^i ~P ( x i^i y ) ) \ { (/) } )
12 unidif0 
 |-  U. ( ( B i^i ~P ( x i^i y ) ) \ { (/) } ) = U. ( B i^i ~P ( x i^i y ) )
13 11 12 eqtri 
 |-  U. ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) = U. ( B i^i ~P ( x i^i y ) )
14 13 sseq2i 
 |-  ( ( x i^i y ) C_ U. ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) <-> ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
15 14 ralbii 
 |-  ( A. y e. ( B \ { (/) } ) ( x i^i y ) C_ U. ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) <-> A. y e. ( B \ { (/) } ) ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
16 inss2 
 |-  ( x i^i y ) C_ y
17 elinel2 
 |-  ( y e. ( B i^i { (/) } ) -> y e. { (/) } )
18 elsni 
 |-  ( y e. { (/) } -> y = (/) )
19 17 18 syl 
 |-  ( y e. ( B i^i { (/) } ) -> y = (/) )
20 0ss 
 |-  (/) C_ U. ( B i^i ~P ( x i^i y ) )
21 19 20 eqsstrdi 
 |-  ( y e. ( B i^i { (/) } ) -> y C_ U. ( B i^i ~P ( x i^i y ) ) )
22 16 21 sstrid 
 |-  ( y e. ( B i^i { (/) } ) -> ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
23 22 rgen 
 |-  A. y e. ( B i^i { (/) } ) ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) )
24 ralunb 
 |-  ( A. y e. ( ( B i^i { (/) } ) u. ( B \ { (/) } ) ) ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> ( A. y e. ( B i^i { (/) } ) ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) /\ A. y e. ( B \ { (/) } ) ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) )
25 23 24 mpbiran 
 |-  ( A. y e. ( ( B i^i { (/) } ) u. ( B \ { (/) } ) ) ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> A. y e. ( B \ { (/) } ) ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
26 inundif 
 |-  ( ( B i^i { (/) } ) u. ( B \ { (/) } ) ) = B
27 26 raleqi 
 |-  ( A. y e. ( ( B i^i { (/) } ) u. ( B \ { (/) } ) ) ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
28 15 25 27 3bitr2i 
 |-  ( A. y e. ( B \ { (/) } ) ( x i^i y ) C_ U. ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) <-> A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
29 28 ralbii 
 |-  ( A. x e. ( B \ { (/) } ) A. y e. ( B \ { (/) } ) ( x i^i y ) C_ U. ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) <-> A. x e. ( B \ { (/) } ) A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
30 inss1 
 |-  ( x i^i y ) C_ x
31 elinel2 
 |-  ( x e. ( B i^i { (/) } ) -> x e. { (/) } )
32 elsni 
 |-  ( x e. { (/) } -> x = (/) )
33 31 32 syl 
 |-  ( x e. ( B i^i { (/) } ) -> x = (/) )
34 33 20 eqsstrdi 
 |-  ( x e. ( B i^i { (/) } ) -> x C_ U. ( B i^i ~P ( x i^i y ) ) )
35 30 34 sstrid 
 |-  ( x e. ( B i^i { (/) } ) -> ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
36 35 ralrimivw 
 |-  ( x e. ( B i^i { (/) } ) -> A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
37 36 rgen 
 |-  A. x e. ( B i^i { (/) } ) A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) )
38 ralunb 
 |-  ( A. x e. ( ( B i^i { (/) } ) u. ( B \ { (/) } ) ) A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> ( A. x e. ( B i^i { (/) } ) A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) /\ A. x e. ( B \ { (/) } ) A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) )
39 37 38 mpbiran 
 |-  ( A. x e. ( ( B i^i { (/) } ) u. ( B \ { (/) } ) ) A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> A. x e. ( B \ { (/) } ) A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
40 26 raleqi 
 |-  ( A. x e. ( ( B i^i { (/) } ) u. ( B \ { (/) } ) ) A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
41 29 39 40 3bitr2i 
 |-  ( A. x e. ( B \ { (/) } ) A. y e. ( B \ { (/) } ) ( x i^i y ) C_ U. ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) )
42 41 a1i 
 |-  ( B e. _V -> ( A. x e. ( B \ { (/) } ) A. y e. ( B \ { (/) } ) ( x i^i y ) C_ U. ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) )
43 difexg 
 |-  ( B e. _V -> ( B \ { (/) } ) e. _V )
44 isbasisg 
 |-  ( ( B \ { (/) } ) e. _V -> ( ( B \ { (/) } ) e. TopBases <-> A. x e. ( B \ { (/) } ) A. y e. ( B \ { (/) } ) ( x i^i y ) C_ U. ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) ) )
45 43 44 syl 
 |-  ( B e. _V -> ( ( B \ { (/) } ) e. TopBases <-> A. x e. ( B \ { (/) } ) A. y e. ( B \ { (/) } ) ( x i^i y ) C_ U. ( ( B \ { (/) } ) i^i ~P ( x i^i y ) ) ) )
46 isbasisg 
 |-  ( B e. _V -> ( B e. TopBases <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) )
47 42 45 46 3bitr4d 
 |-  ( B e. _V -> ( ( B \ { (/) } ) e. TopBases <-> B e. TopBases ) )
48 8 9 47 pm5.21nii 
 |-  ( ( B \ { (/) } ) e. TopBases <-> B e. TopBases )