Metamath Proof Explorer

Theorem kmlem1

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2. (Contributed by NM, 5-Apr-2004)

Ref Expression
Assertion kmlem1 
|- ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. z e. x ps ) -> A. x ( A. z e. x A. w e. x ph -> E. y A. z e. x ( z =/= (/) -> ps ) ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  v e. _V
2 1 rabex 
 |-  { u e. v | u =/= (/) } e. _V
3 raleq 
 |-  ( x = { u e. v | u =/= (/) } -> ( A. z e. x z =/= (/) <-> A. z e. { u e. v | u =/= (/) } z =/= (/) ) )
4 raleq 
 |-  ( x = { u e. v | u =/= (/) } -> ( A. w e. x ph <-> A. w e. { u e. v | u =/= (/) } ph ) )
5 4 raleqbi1dv 
 |-  ( x = { u e. v | u =/= (/) } -> ( A. z e. x A. w e. x ph <-> A. z e. { u e. v | u =/= (/) } A. w e. { u e. v | u =/= (/) } ph ) )
6 3 5 anbi12d 
 |-  ( x = { u e. v | u =/= (/) } -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) <-> ( A. z e. { u e. v | u =/= (/) } z =/= (/) /\ A. z e. { u e. v | u =/= (/) } A. w e. { u e. v | u =/= (/) } ph ) ) )
7 raleq 
 |-  ( x = { u e. v | u =/= (/) } -> ( A. z e. x ps <-> A. z e. { u e. v | u =/= (/) } ps ) )
8 7 exbidv 
 |-  ( x = { u e. v | u =/= (/) } -> ( E. y A. z e. x ps <-> E. y A. z e. { u e. v | u =/= (/) } ps ) )
9 6 8 imbi12d 
 |-  ( x = { u e. v | u =/= (/) } -> ( ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. z e. x ps ) <-> ( ( A. z e. { u e. v | u =/= (/) } z =/= (/) /\ A. z e. { u e. v | u =/= (/) } A. w e. { u e. v | u =/= (/) } ph ) -> E. y A. z e. { u e. v | u =/= (/) } ps ) ) )
10 2 9 spcv 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. z e. x ps ) -> ( ( A. z e. { u e. v | u =/= (/) } z =/= (/) /\ A. z e. { u e. v | u =/= (/) } A. w e. { u e. v | u =/= (/) } ph ) -> E. y A. z e. { u e. v | u =/= (/) } ps ) )
11 10 alrimiv 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. z e. x ps ) -> A. v ( ( A. z e. { u e. v | u =/= (/) } z =/= (/) /\ A. z e. { u e. v | u =/= (/) } A. w e. { u e. v | u =/= (/) } ph ) -> E. y A. z e. { u e. v | u =/= (/) } ps ) )
12 elrabi 
 |-  ( z e. { u e. v | u =/= (/) } -> z e. v )
13 elrabi 
 |-  ( w e. { u e. v | u =/= (/) } -> w e. v )
14 13 imim1i 
 |-  ( ( w e. v -> ph ) -> ( w e. { u e. v | u =/= (/) } -> ph ) )
15 14 ralimi2 
 |-  ( A. w e. v ph -> A. w e. { u e. v | u =/= (/) } ph )
16 12 15 imim12i 
 |-  ( ( z e. v -> A. w e. v ph ) -> ( z e. { u e. v | u =/= (/) } -> A. w e. { u e. v | u =/= (/) } ph ) )
17 16 ralimi2 
 |-  ( A. z e. v A. w e. v ph -> A. z e. { u e. v | u =/= (/) } A. w e. { u e. v | u =/= (/) } ph )
18 neeq1 
 |-  ( u = z -> ( u =/= (/) <-> z =/= (/) ) )
19 18 elrab 
 |-  ( z e. { u e. v | u =/= (/) } <-> ( z e. v /\ z =/= (/) ) )
20 19 simprbi 
 |-  ( z e. { u e. v | u =/= (/) } -> z =/= (/) )
21 20 rgen 
 |-  A. z e. { u e. v | u =/= (/) } z =/= (/)
22 17 21 jctil 
 |-  ( A. z e. v A. w e. v ph -> ( A. z e. { u e. v | u =/= (/) } z =/= (/) /\ A. z e. { u e. v | u =/= (/) } A. w e. { u e. v | u =/= (/) } ph ) )
23 19 biimpri 
 |-  ( ( z e. v /\ z =/= (/) ) -> z e. { u e. v | u =/= (/) } )
24 23 imim1i 
 |-  ( ( z e. { u e. v | u =/= (/) } -> ps ) -> ( ( z e. v /\ z =/= (/) ) -> ps ) )
25 24 expd 
 |-  ( ( z e. { u e. v | u =/= (/) } -> ps ) -> ( z e. v -> ( z =/= (/) -> ps ) ) )
26 25 ralimi2 
 |-  ( A. z e. { u e. v | u =/= (/) } ps -> A. z e. v ( z =/= (/) -> ps ) )
27 26 eximi 
 |-  ( E. y A. z e. { u e. v | u =/= (/) } ps -> E. y A. z e. v ( z =/= (/) -> ps ) )
28 22 27 imim12i 
 |-  ( ( ( A. z e. { u e. v | u =/= (/) } z =/= (/) /\ A. z e. { u e. v | u =/= (/) } A. w e. { u e. v | u =/= (/) } ph ) -> E. y A. z e. { u e. v | u =/= (/) } ps ) -> ( A. z e. v A. w e. v ph -> E. y A. z e. v ( z =/= (/) -> ps ) ) )
29 11 28 sylg 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. z e. x ps ) -> A. v ( A. z e. v A. w e. v ph -> E. y A. z e. v ( z =/= (/) -> ps ) ) )
30 raleq 
 |-  ( v = x -> ( A. w e. v ph <-> A. w e. x ph ) )
31 30 raleqbi1dv 
 |-  ( v = x -> ( A. z e. v A. w e. v ph <-> A. z e. x A. w e. x ph ) )
32 raleq 
 |-  ( v = x -> ( A. z e. v ( z =/= (/) -> ps ) <-> A. z e. x ( z =/= (/) -> ps ) ) )
33 32 exbidv 
 |-  ( v = x -> ( E. y A. z e. v ( z =/= (/) -> ps ) <-> E. y A. z e. x ( z =/= (/) -> ps ) ) )
34 31 33 imbi12d 
 |-  ( v = x -> ( ( A. z e. v A. w e. v ph -> E. y A. z e. v ( z =/= (/) -> ps ) ) <-> ( A. z e. x A. w e. x ph -> E. y A. z e. x ( z =/= (/) -> ps ) ) ) )
35 34 cbvalvw 
 |-  ( A. v ( A. z e. v A. w e. v ph -> E. y A. z e. v ( z =/= (/) -> ps ) ) <-> A. x ( A. z e. x A. w e. x ph -> E. y A. z e. x ( z =/= (/) -> ps ) ) )
36 29 35 sylib 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. z e. x ps ) -> A. x ( A. z e. x A. w e. x ph -> E. y A. z e. x ( z =/= (/) -> ps ) ) )