Metamath Proof Explorer

Theorem kmlem16

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4 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 kmlem16 
|- ( ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) \/ E. y ( -. y e. x /\ ch ) ) <-> E. y A. z E. v A. u ( ( y e. x /\ ph ) \/ ( -. 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 1 2 3 kmlem14 
 |-  ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) <-> E. y A. z E. v A. u ( y e. x /\ ph ) )
5 1 2 3 kmlem15 
 |-  ( ( -. y e. x /\ ch ) <-> A. z E. v A. u ( -. y e. x /\ ps ) )
6 5 exbii 
 |-  ( E. y ( -. y e. x /\ ch ) <-> E. y A. z E. v A. u ( -. y e. x /\ ps ) )
7 4 6 orbi12i 
 |-  ( ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) \/ E. y ( -. y e. x /\ ch ) ) <-> ( E. y A. z E. v A. u ( y e. x /\ ph ) \/ E. y A. z E. v A. u ( -. y e. x /\ ps ) ) )
8 19.43 
 |-  ( E. y ( A. z E. v A. u ( y e. x /\ ph ) \/ A. z E. v A. u ( -. y e. x /\ ps ) ) <-> ( E. y A. z E. v A. u ( y e. x /\ ph ) \/ E. y A. z E. v A. u ( -. y e. x /\ ps ) ) )
9 pm3.24 
 |-  -. ( y e. x /\ -. y e. x )
10 simpl 
 |-  ( ( y e. x /\ ph ) -> y e. x )
11 10 sps 
 |-  ( A. u ( y e. x /\ ph ) -> y e. x )
12 11 exlimivv 
 |-  ( E. z E. v A. u ( y e. x /\ ph ) -> y e. x )
13 simpl 
 |-  ( ( -. y e. x /\ ps ) -> -. y e. x )
14 13 sps 
 |-  ( A. u ( -. y e. x /\ ps ) -> -. y e. x )
15 14 exlimivv 
 |-  ( E. z E. v A. u ( -. y e. x /\ ps ) -> -. y e. x )
16 12 15 anim12i 
 |-  ( ( E. z E. v A. u ( y e. x /\ ph ) /\ E. z E. v A. u ( -. y e. x /\ ps ) ) -> ( y e. x /\ -. y e. x ) )
17 9 16 mto 
 |-  -. ( E. z E. v A. u ( y e. x /\ ph ) /\ E. z E. v A. u ( -. y e. x /\ ps ) )
18 19.33b 
 |-  ( -. ( E. z E. v A. u ( y e. x /\ ph ) /\ E. z E. v A. u ( -. y e. x /\ ps ) ) -> ( A. z ( E. v A. u ( y e. x /\ ph ) \/ E. v A. u ( -. y e. x /\ ps ) ) <-> ( A. z E. v A. u ( y e. x /\ ph ) \/ A. z E. v A. u ( -. y e. x /\ ps ) ) ) )
19 17 18 ax-mp 
 |-  ( A. z ( E. v A. u ( y e. x /\ ph ) \/ E. v A. u ( -. y e. x /\ ps ) ) <-> ( A. z E. v A. u ( y e. x /\ ph ) \/ A. z E. v A. u ( -. y e. x /\ ps ) ) )
20 10 exlimiv 
 |-  ( E. u ( y e. x /\ ph ) -> y e. x )
21 13 exlimiv 
 |-  ( E. u ( -. y e. x /\ ps ) -> -. y e. x )
22 20 21 anim12i 
 |-  ( ( E. u ( y e. x /\ ph ) /\ E. u ( -. y e. x /\ ps ) ) -> ( y e. x /\ -. y e. x ) )
23 9 22 mto 
 |-  -. ( E. u ( y e. x /\ ph ) /\ E. u ( -. y e. x /\ ps ) )
24 19.33b 
 |-  ( -. ( E. u ( y e. x /\ ph ) /\ E. u ( -. y e. x /\ ps ) ) -> ( A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) <-> ( A. u ( y e. x /\ ph ) \/ A. u ( -. y e. x /\ ps ) ) ) )
25 23 24 ax-mp 
 |-  ( A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) <-> ( A. u ( y e. x /\ ph ) \/ A. u ( -. y e. x /\ ps ) ) )
26 25 exbii 
 |-  ( E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) <-> E. v ( A. u ( y e. x /\ ph ) \/ A. u ( -. y e. x /\ ps ) ) )
27 19.43 
 |-  ( E. v ( A. u ( y e. x /\ ph ) \/ A. u ( -. y e. x /\ ps ) ) <-> ( E. v A. u ( y e. x /\ ph ) \/ E. v A. u ( -. y e. x /\ ps ) ) )
28 26 27 bitr2i 
 |-  ( ( E. v A. u ( y e. x /\ ph ) \/ E. v A. u ( -. y e. x /\ ps ) ) <-> E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) )
29 28 albii 
 |-  ( A. z ( E. v A. u ( y e. x /\ ph ) \/ E. v A. u ( -. y e. x /\ ps ) ) <-> A. z E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) )
30 19 29 bitr3i 
 |-  ( ( A. z E. v A. u ( y e. x /\ ph ) \/ A. z E. v A. u ( -. y e. x /\ ps ) ) <-> A. z E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) )
31 30 exbii 
 |-  ( E. y ( A. z E. v A. u ( y e. x /\ ph ) \/ A. z E. v A. u ( -. y e. x /\ ps ) ) <-> E. y A. z E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) )
32 7 8 31 3bitr2i 
 |-  ( ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) \/ E. y ( -. y e. x /\ ch ) ) <-> E. y A. z E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) )