Theorem kmlem15 8986

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

Hypotheses

Ref	Expression
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

Ref	Expression
kmlem15	|- ( ( -. y e. x /\ ch ) <-> A. z E. v A. u ( -. y e. x /\ ps ) )

Distinct variable groups:   x, y, z, v, u   ph, u

Allowed substitution hints:   ph( x, y, z, v)   ps( x, y, z, v, u)   ch( x, y, z, v, u)

Proof of Theorem kmlem15

Step	Hyp	Ref	Expression
1		kmlem14.3	. . . 4 |- ( ch <-> A. z e. x E! v v e. ( z i^i y ) )
2		nfv 1843	. . . . . . 7 |- F/ u v e. ( z i^i y )
3	2	eu1 2510	. . . . . 6 |- ( 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 ) ) )
4		elin 3796	. . . . . . . . 9 |- ( v e. ( z i^i y ) <-> ( v e. z /\ v e. y ) )
5		clelsb3 2729	. . . . . . . . . . . 12 |- ( [ u / v ] v e. ( z i^i y ) <-> u e. ( z i^i y ) )
6		elin 3796	. . . . . . . . . . . 12 |- ( u e. ( z i^i y ) <-> ( u e. z /\ u e. y ) )
7	5, 6	bitri 264	. . . . . . . . . . 11 |- ( [ u / v ] v e. ( z i^i y ) <-> ( u e. z /\ u e. y ) )
8		equcom 1945	. . . . . . . . . . 11 |- ( v = u <-> u = v )
9	7, 8	imbi12i 340	. . . . . . . . . 10 |- ( ( [ u / v ] v e. ( z i^i y ) -> v = u ) <-> ( ( u e. z /\ u e. y ) -> u = v ) )
10	9	albii 1747	. . . . . . . . 9 |- ( A. u ( [ u / v ] v e. ( z i^i y ) -> v = u ) <-> A. u ( ( u e. z /\ u e. y ) -> u = v ) )
11	4, 10	anbi12i 733	. . . . . . . 8 |- ( ( 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 ) ) )
12		19.28v 1909	. . . . . . . 8 |- ( 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 ) ) )
13	11, 12	bitr4i 267	. . . . . . 7 |- ( ( 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 ) ) )
14	13	exbii 1774	. . . . . 6 |- ( 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 ) ) )
15	3, 14	bitri 264	. . . . 5 |- ( 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 ) ) )
16	15	ralbii 2980	. . . 4 |- ( 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 ) ) )
17		df-ral 2917	. . . . 5 |- ( 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 ) ) ) )
18		kmlem14.2	. . . . . . . . . 10 |- ( ps <-> ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
19	18	albii 1747	. . . . . . . . 9 |- ( A. u ps <-> A. u ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
20		19.21v 1868	. . . . . . . . 9 |- ( 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 ) ) ) )
21	19, 20	bitri 264	. . . . . . . 8 |- ( A. u ps <-> ( z e. x -> A. u ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
22	21	exbii 1774	. . . . . . 7 |- ( 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 ) ) ) )
23		19.37v 1910	. . . . . . 7 |- ( 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 ) ) ) )
24	22, 23	bitri 264	. . . . . 6 |- ( 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 ) ) ) )
25	24	albii 1747	. . . . 5 |- ( 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 ) ) ) )
26	17, 25	bitr4i 267	. . . 4 |- ( 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 )
27	1, 16, 26	3bitri 286	. . 3 |- ( ch <-> A. z E. v A. u ps )
28	27	anbi2i 730	. 2 |- ( ( -. y e. x /\ ch ) <-> ( -. y e. x /\ A. z E. v A. u ps ) )
29		19.28v 1909	. 2 |- ( A. z ( -. y e. x /\ E. v A. u ps ) <-> ( -. y e. x /\ A. z E. v A. u ps ) )
30		19.28v 1909	. . . . 5 |- ( A. u ( -. y e. x /\ ps ) <-> ( -. y e. x /\ A. u ps ) )
31	30	exbii 1774	. . . 4 |- ( E. v A. u ( -. y e. x /\ ps ) <-> E. v ( -. y e. x /\ A. u ps ) )
32		19.42v 1918	. . . 4 |- ( E. v ( -. y e. x /\ A. u ps ) <-> ( -. y e. x /\ E. v A. u ps ) )
33	31, 32	bitr2i 265	. . 3 |- ( ( -. y e. x /\ E. v A. u ps ) <-> E. v A. u ( -. y e. x /\ ps ) )
34	33	albii 1747	. 2 |- ( A. z ( -. y e. x /\ E. v A. u ps ) <-> A. z E. v A. u ( -. y e. x /\ ps ) )
35	28, 29, 34	3bitr2i 288	1 |- ( ( -. y e. x /\ ch ) <-> A. z E. v A. u ( -. y e. x /\ ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704   [wsb 1880   e. wcel 1990   E!weu 2470   =/= wne 2794   A.wral 2912   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-in 3581

This theorem is referenced by:  kmlem16  8987