Theorem kmlem14 8985

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
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 ) )

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

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

Proof of Theorem kmlem14

Step	Hyp	Ref	Expression
1		neeq1 2856	. . . . . 6 |- ( z = y -> ( z =/= w <-> y =/= w ) )
2		ineq1 3807	. . . . . . 7 |- ( z = y -> ( z i^i w ) = ( y i^i w ) )
3	2	eleq2d 2687	. . . . . 6 |- ( z = y -> ( v e. ( z i^i w ) <-> v e. ( y i^i w ) ) )
4	1, 3	anbi12d 747	. . . . 5 |- ( z = y -> ( ( z =/= w /\ v e. ( z i^i w ) ) <-> ( y =/= w /\ v e. ( y i^i w ) ) ) )
5	4	rexbidv 3052	. . . 4 |- ( z = y -> ( E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) <-> E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) ) )
6	5	raleqbi1dv 3146	. . 3 |- ( z = y -> ( A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) <-> A. v e. y E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) ) )
7	6	cbvrexv 3172	. 2 |- ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) <-> E. y e. x A. v e. y E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) )
8		df-rex 2918	. 2 |- ( E. y e. x A. v e. y E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) <-> E. y ( y e. x /\ A. v e. y E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) ) )
9		eleq1 2689	. . . . . . . . 9 |- ( v = z -> ( v e. ( y i^i w ) <-> z e. ( y i^i w ) ) )
10	9	anbi2d 740	. . . . . . . 8 |- ( v = z -> ( ( y =/= w /\ v e. ( y i^i w ) ) <-> ( y =/= w /\ z e. ( y i^i w ) ) ) )
11	10	rexbidv 3052	. . . . . . 7 |- ( v = z -> ( E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) <-> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) )
12	11	cbvralv 3171	. . . . . 6 |- ( A. v e. y E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) <-> A. z e. y E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) )
13		df-ral 2917	. . . . . 6 |- ( A. z e. y E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) <-> A. z ( z e. y -> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) )
14	12, 13	bitri 264	. . . . 5 |- ( A. v e. y E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) <-> A. z ( z e. y -> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) )
15	14	anbi2i 730	. . . 4 |- ( ( y e. x /\ A. v e. y E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) ) <-> ( y e. x /\ A. z ( z e. y -> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) ) )
16		19.28v 1909	. . . 4 |- ( A. z ( y e. x /\ ( z e. y -> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) ) <-> ( y e. x /\ A. z ( z e. y -> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) ) )
17		neeq2 2857	. . . . . . . . . . . 12 |- ( w = v -> ( y =/= w <-> y =/= v ) )
18		ineq2 3808	. . . . . . . . . . . . 13 |- ( w = v -> ( y i^i w ) = ( y i^i v ) )
19	18	eleq2d 2687	. . . . . . . . . . . 12 |- ( w = v -> ( z e. ( y i^i w ) <-> z e. ( y i^i v ) ) )
20	17, 19	anbi12d 747	. . . . . . . . . . 11 |- ( w = v -> ( ( y =/= w /\ z e. ( y i^i w ) ) <-> ( y =/= v /\ z e. ( y i^i v ) ) ) )
21	20	cbvrexv 3172	. . . . . . . . . 10 |- ( E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) <-> E. v e. x ( y =/= v /\ z e. ( y i^i v ) ) )
22		df-rex 2918	. . . . . . . . . 10 |- ( E. v e. x ( y =/= v /\ z e. ( y i^i v ) ) <-> E. v ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) )
23	21, 22	bitri 264	. . . . . . . . 9 |- ( E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) <-> E. v ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) )
24	23	imbi2i 326	. . . . . . . 8 |- ( ( z e. y -> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) <-> ( z e. y -> E. v ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) )
25		19.37v 1910	. . . . . . . 8 |- ( E. v ( z e. y -> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) <-> ( z e. y -> E. v ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) )
26	24, 25	bitr4i 267	. . . . . . 7 |- ( ( z e. y -> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) <-> E. v ( z e. y -> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) )
27	26	anbi2i 730	. . . . . 6 |- ( ( y e. x /\ ( z e. y -> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) ) <-> ( y e. x /\ E. v ( z e. y -> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) ) )
28		19.42v 1918	. . . . . 6 |- ( E. v ( y e. x /\ ( z e. y -> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) ) <-> ( y e. x /\ E. v ( z e. y -> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) ) )
29		19.3v 1897	. . . . . . . 8 |- ( A. u ( y e. x /\ ph ) <-> ( y e. x /\ ph ) )
30		kmlem14.1	. . . . . . . . . 10 |- ( ph <-> ( z e. y -> ( ( v e. x /\ y =/= v ) /\ z e. v ) ) )
31		elin 3796	. . . . . . . . . . . . . 14 |- ( z e. ( y i^i v ) <-> ( z e. y /\ z e. v ) )
32	31	baibr 945	. . . . . . . . . . . . 13 |- ( z e. y -> ( z e. v <-> z e. ( y i^i v ) ) )
33	32	anbi2d 740	. . . . . . . . . . . 12 |- ( z e. y -> ( ( ( v e. x /\ y =/= v ) /\ z e. v ) <-> ( ( v e. x /\ y =/= v ) /\ z e. ( y i^i v ) ) ) )
34		anass 681	. . . . . . . . . . . 12 |- ( ( ( v e. x /\ y =/= v ) /\ z e. ( y i^i v ) ) <-> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) )
35	33, 34	syl6bb 276	. . . . . . . . . . 11 |- ( z e. y -> ( ( ( v e. x /\ y =/= v ) /\ z e. v ) <-> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) )
36	35	pm5.74i 260	. . . . . . . . . 10 |- ( ( z e. y -> ( ( v e. x /\ y =/= v ) /\ z e. v ) ) <-> ( z e. y -> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) )
37	30, 36	bitri 264	. . . . . . . . 9 |- ( ph <-> ( z e. y -> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) )
38	37	anbi2i 730	. . . . . . . 8 |- ( ( y e. x /\ ph ) <-> ( y e. x /\ ( z e. y -> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) ) )
39	29, 38	bitr2i 265	. . . . . . 7 |- ( ( y e. x /\ ( z e. y -> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) ) <-> A. u ( y e. x /\ ph ) )
40	39	exbii 1774	. . . . . 6 |- ( E. v ( y e. x /\ ( z e. y -> ( v e. x /\ ( y =/= v /\ z e. ( y i^i v ) ) ) ) ) <-> E. v A. u ( y e. x /\ ph ) )
41	27, 28, 40	3bitr2i 288	. . . . 5 |- ( ( y e. x /\ ( z e. y -> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) ) <-> E. v A. u ( y e. x /\ ph ) )
42	41	albii 1747	. . . 4 |- ( A. z ( y e. x /\ ( z e. y -> E. w e. x ( y =/= w /\ z e. ( y i^i w ) ) ) ) <-> A. z E. v A. u ( y e. x /\ ph ) )
43	15, 16, 42	3bitr2i 288	. . 3 |- ( ( y e. x /\ A. v e. y E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) ) <-> A. z E. v A. u ( y e. x /\ ph ) )
44	43	exbii 1774	. 2 |- ( E. y ( y e. x /\ A. v e. y E. w e. x ( y =/= w /\ v e. ( y i^i w ) ) ) <-> E. y A. z E. v A. u ( y e. x /\ ph ) )
45	7, 8, 44	3bitri 286	1 |- ( 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 ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704   e. wcel 1990   E!weu 2470   =/= wne 2794   A.wral 2912   E.wrex 2913   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-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581

This theorem is referenced by:  kmlem16  8987