Metamath Proof Explorer

Theorem kmlem15

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

Ref Expression
Hypotheses kmlem14.1 
|- ( ph <-> ( z e. y -> ( ( v e. x /\ y =/= v ) /\ z e. v ) ) )
kmlem14.2 
|- ( ps <-> ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
kmlem14.3 
|- ( ch <-> A. z e. x E! v v e. ( z i^i y ) )
Assertion kmlem15 
|- ( ( -. y e. x /\ ch ) <-> A. z E. v A. u ( -. y e. x /\ ps ) )

Proof

Step Hyp Ref Expression
1 kmlem14.1 
 |-  ( ph <-> ( z e. y -> ( ( v e. x /\ y =/= v ) /\ z e. v ) ) )
2 kmlem14.2 
 |-  ( ps <-> ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
3 kmlem14.3 
 |-  ( ch <-> A. z e. x E! v v e. ( z i^i y ) )
4 nfv 
 |-  F/ u v e. ( z i^i y )
5 4 eu1 
 |-  ( E! v v e. ( z i^i y ) <-> E. v ( v e. ( z i^i y ) /\ A. u ( [ u / v ] v e. ( z i^i y ) -> v = u ) ) )
6 elin 
 |-  ( v e. ( z i^i y ) <-> ( v e. z /\ v e. y ) )
7 clelsb3 
 |-  ( [ u / v ] v e. ( z i^i y ) <-> u e. ( z i^i y ) )
8 elin 
 |-  ( u e. ( z i^i y ) <-> ( u e. z /\ u e. y ) )
9 7 8 bitri 
 |-  ( [ u / v ] v e. ( z i^i y ) <-> ( u e. z /\ u e. y ) )
10 equcom 
 |-  ( v = u <-> u = v )
11 9 10 imbi12i 
 |-  ( ( [ u / v ] v e. ( z i^i y ) -> v = u ) <-> ( ( u e. z /\ u e. y ) -> u = v ) )
12 11 albii 
 |-  ( A. u ( [ u / v ] v e. ( z i^i y ) -> v = u ) <-> A. u ( ( u e. z /\ u e. y ) -> u = v ) )
13 6 12 anbi12i 
 |-  ( ( v e. ( z i^i y ) /\ A. u ( [ u / v ] v e. ( z i^i y ) -> v = u ) ) <-> ( ( v e. z /\ v e. y ) /\ A. u ( ( u e. z /\ u e. y ) -> u = v ) ) )
14 19.28v 
 |-  ( A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) <-> ( ( v e. z /\ v e. y ) /\ A. u ( ( u e. z /\ u e. y ) -> u = v ) ) )
15 13 14 bitr4i 
 |-  ( ( v e. ( z i^i y ) /\ A. u ( [ u / v ] v e. ( z i^i y ) -> v = u ) ) <-> A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) )
16 15 exbii 
 |-  ( E. v ( v e. ( z i^i y ) /\ A. u ( [ u / v ] v e. ( z i^i y ) -> v = u ) ) <-> E. v A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) )
17 5 16 bitri 
 |-  ( E! v v e. ( z i^i y ) <-> E. v A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) )
18 17 ralbii 
 |-  ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. x E. v A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) )
19 df-ral 
 |-  ( A. z e. x E. v A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) <-> A. z ( z e. x -> E. v A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
20 2 albii 
 |-  ( A. u ps <-> A. u ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
21 19.21v 
 |-  ( A. u ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) <-> ( z e. x -> A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
22 20 21 bitri 
 |-  ( A. u ps <-> ( z e. x -> A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
23 22 exbii 
 |-  ( E. v A. u ps <-> E. v ( z e. x -> A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
24 19.37v 
 |-  ( E. v ( z e. x -> A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) <-> ( z e. x -> E. v A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
25 23 24 bitri 
 |-  ( E. v A. u ps <-> ( z e. x -> E. v A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
26 25 albii 
 |-  ( A. z E. v A. u ps <-> A. z ( z e. x -> E. v A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
27 19 26 bitr4i 
 |-  ( A. z e. x E. v A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) <-> A. z E. v A. u ps )
28 3 18 27 3bitri 
 |-  ( ch <-> A. z E. v A. u ps )
29 28 anbi2i 
 |-  ( ( -. y e. x /\ ch ) <-> ( -. y e. x /\ A. z E. v A. u ps ) )
30 19.28v 
 |-  ( A. z ( -. y e. x /\ E. v A. u ps ) <-> ( -. y e. x /\ A. z E. v A. u ps ) )
31 19.28v 
 |-  ( A. u ( -. y e. x /\ ps ) <-> ( -. y e. x /\ A. u ps ) )
32 31 exbii 
 |-  ( E. v A. u ( -. y e. x /\ ps ) <-> E. v ( -. y e. x /\ A. u ps ) )
33 19.42v 
 |-  ( E. v ( -. y e. x /\ A. u ps ) <-> ( -. y e. x /\ E. v A. u ps ) )
34 32 33 bitr2i 
 |-  ( ( -. y e. x /\ E. v A. u ps ) <-> E. v A. u ( -. y e. x /\ ps ) )
35 34 albii 
 |-  ( A. z ( -. y e. x /\ E. v A. u ps ) <-> A. z E. v A. u ( -. y e. x /\ ps ) )
36 29 30 35 3bitr2i 
 |-  ( ( -. y e. x /\ ch ) <-> A. z E. v A. u ( -. y e. x /\ ps ) )