Metamath Proof Explorer

Theorem cplem2

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

Ref Expression
Hypothesis cplem2.1 
|- A e. _V
Assertion cplem2 
|- E. y A. x e. A ( B =/= (/) -> ( B i^i y ) =/= (/) )

Proof

Step Hyp Ref Expression
1 cplem2.1 
 |-  A e. _V
2 scottex 
 |-  { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } e. _V
3 1 2 iunex 
 |-  U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } e. _V
4 nfiu1 
 |-  F/_ x U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) }
5 4 nfeq2 
 |-  F/ x y = U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) }
6 ineq2 
 |-  ( y = U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } -> ( B i^i y ) = ( B i^i U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } ) )
7 6 neeq1d 
 |-  ( y = U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } -> ( ( B i^i y ) =/= (/) <-> ( B i^i U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } ) =/= (/) ) )
8 7 imbi2d 
 |-  ( y = U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } -> ( ( B =/= (/) -> ( B i^i y ) =/= (/) ) <-> ( B =/= (/) -> ( B i^i U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } ) =/= (/) ) ) )
9 5 8 ralbid 
 |-  ( y = U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } -> ( A. x e. A ( B =/= (/) -> ( B i^i y ) =/= (/) ) <-> A. x e. A ( B =/= (/) -> ( B i^i U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } ) =/= (/) ) ) )
10 eqid 
 |-  { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } = { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) }
11 eqid 
 |-  U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } = U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) }
12 10 11 cplem1 
 |-  A. x e. A ( B =/= (/) -> ( B i^i U_ x e. A { z e. B | A. w e. B ( rank ` z ) C_ ( rank ` w ) } ) =/= (/) )
13 3 9 12 ceqsexv2d 
 |-  E. y A. x e. A ( B =/= (/) -> ( B i^i y ) =/= (/) )