This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid 
 |-  ( x e. A -> ( B =/= (/) -> ( B i^i D ) =/= (/) ) )
20 19 rgen 
 |-  A. x e. A ( B =/= (/) -> ( B i^i D ) =/= (/) )