Theorem basis1

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

	Ref	Expression
Assertion	basis1	|- ( ( B e. TopBases /\ C e. B /\ D e. B ) -> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) )

Proof

Step	Hyp	Ref	Expression
1		isbasisg	|- ( B e. TopBases -> ( 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 ) ) ) )
2	1	ibi	|- ( 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 ) ) )
3		ineq1	|- ( x = C -> ( x i^i y ) = ( C i^i y ) )
4	3	pweqd	|- ( x = C -> ~P ( x i^i y ) = ~P ( C i^i y ) )
5	4	ineq2d	|- ( x = C -> ( B i^i ~P ( x i^i y ) ) = ( B i^i ~P ( C i^i y ) ) )
6	5	unieqd	|- ( x = C -> U. ( B i^i ~P ( x i^i y ) ) = U. ( B i^i ~P ( C i^i y ) ) )
7	3 6	sseq12d	|- ( x = C -> ( ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> ( C i^i y ) C_ U. ( B i^i ~P ( C i^i y ) ) ) )
8		ineq2	|- ( y = D -> ( C i^i y ) = ( C i^i D ) )
9	8	pweqd	|- ( y = D -> ~P ( C i^i y ) = ~P ( C i^i D ) )
10	9	ineq2d	|- ( y = D -> ( B i^i ~P ( C i^i y ) ) = ( B i^i ~P ( C i^i D ) ) )
11	10	unieqd	|- ( y = D -> U. ( B i^i ~P ( C i^i y ) ) = U. ( B i^i ~P ( C i^i D ) ) )
12	8 11	sseq12d	|- ( y = D -> ( ( C i^i y ) C_ U. ( B i^i ~P ( C i^i y ) ) <-> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) ) )
13	7 12	rspc2v	|- ( ( C e. B /\ D e. B ) -> ( A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) -> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) ) )
14	2 13	syl5com	|- ( B e. TopBases -> ( ( C e. B /\ D e. B ) -> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) ) )
15	14	3impib	|- ( ( B e. TopBases /\ C e. B /\ D e. B ) -> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) )