Metamath Proof Explorer

Theorem basis2

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

Ref Expression
Assertion basis2 
|- ( ( ( B e. TopBases /\ C e. B ) /\ ( D e. B /\ A e. ( C i^i D ) ) ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) )

Proof

Step Hyp Ref Expression
1 isbasis2g 
 |-  ( B e. TopBases -> ( B e. TopBases <-> A. y e. B A. z e. B A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) ) )
2 1 ibi 
 |-  ( B e. TopBases -> A. y e. B A. z e. B A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) )
3 ineq1 
 |-  ( y = C -> ( y i^i z ) = ( C i^i z ) )
4 sseq2 
 |-  ( ( y i^i z ) = ( C i^i z ) -> ( x C_ ( y i^i z ) <-> x C_ ( C i^i z ) ) )
5 4 anbi2d 
 |-  ( ( y i^i z ) = ( C i^i z ) -> ( ( w e. x /\ x C_ ( y i^i z ) ) <-> ( w e. x /\ x C_ ( C i^i z ) ) ) )
6 5 rexbidv 
 |-  ( ( y i^i z ) = ( C i^i z ) -> ( E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) <-> E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) ) )
7 6 raleqbi1dv 
 |-  ( ( y i^i z ) = ( C i^i z ) -> ( A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) <-> A. w e. ( C i^i z ) E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) ) )
8 3 7 syl 
 |-  ( y = C -> ( A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) <-> A. w e. ( C i^i z ) E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) ) )
9 ineq2 
 |-  ( z = D -> ( C i^i z ) = ( C i^i D ) )
10 sseq2 
 |-  ( ( C i^i z ) = ( C i^i D ) -> ( x C_ ( C i^i z ) <-> x C_ ( C i^i D ) ) )
11 10 anbi2d 
 |-  ( ( C i^i z ) = ( C i^i D ) -> ( ( w e. x /\ x C_ ( C i^i z ) ) <-> ( w e. x /\ x C_ ( C i^i D ) ) ) )
12 11 rexbidv 
 |-  ( ( C i^i z ) = ( C i^i D ) -> ( E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) <-> E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) ) )
13 12 raleqbi1dv 
 |-  ( ( C i^i z ) = ( C i^i D ) -> ( A. w e. ( C i^i z ) E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) <-> A. w e. ( C i^i D ) E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) ) )
14 9 13 syl 
 |-  ( z = D -> ( A. w e. ( C i^i z ) E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) <-> A. w e. ( C i^i D ) E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) ) )
15 8 14 rspc2v 
 |-  ( ( C e. B /\ D e. B ) -> ( A. y e. B A. z e. B A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) -> A. w e. ( C i^i D ) E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) ) )
16 eleq1 
 |-  ( w = A -> ( w e. x <-> A e. x ) )
17 16 anbi1d 
 |-  ( w = A -> ( ( w e. x /\ x C_ ( C i^i D ) ) <-> ( A e. x /\ x C_ ( C i^i D ) ) ) )
18 17 rexbidv 
 |-  ( w = A -> ( E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) <-> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) )
19 18 rspccv 
 |-  ( A. w e. ( C i^i D ) E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) -> ( A e. ( C i^i D ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) )
20 15 19 syl6com 
 |-  ( A. y e. B A. z e. B A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) -> ( ( C e. B /\ D e. B ) -> ( A e. ( C i^i D ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) ) )
21 2 20 syl 
 |-  ( B e. TopBases -> ( ( C e. B /\ D e. B ) -> ( A e. ( C i^i D ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) ) )
22 21 expd 
 |-  ( B e. TopBases -> ( C e. B -> ( D e. B -> ( A e. ( C i^i D ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) ) ) )
23 22 imp43 
 |-  ( ( ( B e. TopBases /\ C e. B ) /\ ( D e. B /\ A e. ( C i^i D ) ) ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) )