Theorem cplem1

Description: Lemma for the Collection Principle cp . (Contributed by NM, 17-Oct-2003) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026)

	Ref	Expression
Hypothesis	cplem1.1	|- C = U_ x e. A Scott B
Assertion	cplem1	|- A. x e. A ( B =/= (/) -> ( B i^i C ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		cplem1.1	|- C = U_ x e. A Scott B
2		scott0b	|- ( B = (/) <-> Scott B = (/) )
3	2	necon3bii	|- ( B =/= (/) <-> Scott B =/= (/) )
4		n0	|- ( Scott B =/= (/) <-> E. y y e. Scott B )
5	3 4	bitri	|- ( B =/= (/) <-> E. y y e. Scott B )
6		scottss	|- Scott B C_ B
7	6	sseli	|- ( y e. Scott B -> y e. B )
8	7	a1i	|- ( x e. A -> ( y e. Scott B -> y e. B ) )
9		ssiun2	|- ( x e. A -> Scott B C_ U_ x e. A Scott B )
10	9 1	sseqtrrdi	|- ( x e. A -> Scott B C_ C )
11	10	sseld	|- ( x e. A -> ( y e. Scott B -> y e. C ) )
12	8 11	jcad	|- ( x e. A -> ( y e. Scott B -> ( y e. B /\ y e. C ) ) )
13		inelcm	|- ( ( y e. B /\ y e. C ) -> ( B i^i C ) =/= (/) )
14	12 13	syl6	|- ( x e. A -> ( y e. Scott B -> ( B i^i C ) =/= (/) ) )
15	14	exlimdv	|- ( x e. A -> ( E. y y e. Scott B -> ( B i^i C ) =/= (/) ) )
16	5 15	biimtrid	|- ( x e. A -> ( B =/= (/) -> ( B i^i C ) =/= (/) ) )
17	16	rgen	|- A. x e. A ( B =/= (/) -> ( B i^i C ) =/= (/) )