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

Metamath Proof Explorer

Theorem kmlem10

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004)

Ref Expression
Hypothesis kmlem9.1 
|- A = { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) }
Assertion kmlem10 
|- ( A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ph ) -> E. y A. z e. A ph )

Proof

Step Hyp Ref Expression
1 kmlem9.1 
 |-  A = { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) }
2 1 kmlem9 
 |-  A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) )
3 vex 
 |-  x e. _V
4 3 abrexex 
 |-  { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) } e. _V
5 1 4 eqeltri 
 |-  A e. _V
6 raleq 
 |-  ( h = A -> ( A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) <-> A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) ) )
7 6 raleqbi1dv 
 |-  ( h = A -> ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) <-> A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) ) )
8 raleq 
 |-  ( h = A -> ( A. z e. h ph <-> A. z e. A ph ) )
9 8 exbidv 
 |-  ( h = A -> ( E. y A. z e. h ph <-> E. y A. z e. A ph ) )
10 7 9 imbi12d 
 |-  ( h = A -> ( ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ph ) <-> ( A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. A ph ) ) )
11 5 10 spcv 
 |-  ( A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ph ) -> ( A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. A ph ) )
12 2 11 mpi 
 |-  ( A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ph ) -> E. y A. z e. A ph )