Theorem cplem1

Description: Lemma for the Collection Principle cp . (Contributed by NM, 17-Oct-2003)

	Ref	Expression
Hypotheses	cplem1.1	|- C = { y e. B | A. z e. B ( rank ` y ) C_ ( rank ` z ) }
	cplem1.2	|- D = U_ x e. A C
Assertion	cplem1	|- A. x e. A ( B =/= (/) -> ( B i^i D ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		cplem1.1	|- C = { y e. B | A. z e. B ( rank ` y ) C_ ( rank ` z ) }
2		cplem1.2	|- D = U_ x e. A C
3		scott0	|- ( B = (/) <-> { y e. B | A. z e. B ( rank ` y ) C_ ( rank ` z ) } = (/) )
4	1	eqeq1i	|- ( C = (/) <-> { y e. B | A. z e. B ( rank ` y ) C_ ( rank ` z ) } = (/) )
5	3 4	bitr4i	|- ( B = (/) <-> C = (/) )
6	5	necon3bii	|- ( B =/= (/) <-> C =/= (/) )
7		n0	|- ( C =/= (/) <-> E. w w e. C )
8	6 7	bitri	|- ( B =/= (/) <-> E. w w e. C )
9	1	ssrab3	|- C C_ B
10	9	sseli	|- ( w e. C -> w e. B )
11	10	a1i	|- ( x e. A -> ( w e. C -> w e. B ) )
12		ssiun2	|- ( x e. A -> C C_ U_ x e. A C )
13	12 2	sseqtrrdi	|- ( x e. A -> C C_ D )
14	13	sseld	|- ( x e. A -> ( w e. C -> w e. D ) )
15	11 14	jcad	|- ( x e. A -> ( w e. C -> ( w e. B /\ w e. D ) ) )
16		inelcm	|- ( ( w e. B /\ w e. D ) -> ( B i^i D ) =/= (/) )
17	15 16	syl6	|- ( x e. A -> ( w e. C -> ( B i^i D ) =/= (/) ) )
18	17	exlimdv	|- ( x e. A -> ( E. w w e. C -> ( B i^i D ) =/= (/) ) )
19	8 18	syl5bi	|- ( x e. A -> ( B =/= (/) -> ( B i^i D ) =/= (/) ) )
20	19	rgen	|- A. x e. A ( B =/= (/) -> ( B i^i D ) =/= (/) )