Theorem kmlem14 4778

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4.

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.yA.zE.vA.u(y e. x /\ ph))

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

Proof of Theorem kmlem14

Step	Hyp	Ref	Expression
1		neeq1 1590	. . . . . 6 |- (z = y -> (z =/= w <-> y =/= w))
2		ineq1 2210	. . . . . . 7 |- (z = y -> (z i^i w) = (y i^i w))
3	2	eleq2d 1541	. . . . . 6 |- (z = y -> (v e. (z i^i w) <-> v e. (y i^i w)))
4	1, 3	anbi12d 628	. . . . 5 |- (z = y -> ((z =/= w /\ v e. (z i^i w)) <-> (y =/= w /\ v e. (y i^i w))))
5	4	rexbidv 1664	. . . 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	raleqd 1791	. . 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 1801	. 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 1650	. 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 1534	. . . . . . . . 9 |- (v = z -> (v e. (y i^i w) <-> z e. (y i^i w)))
10	9	anbi2d 616	. . . . . . . 8 |- (v = z -> ((y =/= w /\ v e. (y i^i w)) <-> (y =/= w /\ z e. (y i^i w))))
11	10	rexbidv 1664	. . . . . . 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 1800	. . . . . 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 1649	. . . . . 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	bitr 173	. . . . 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 480	. . . 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 1299	. . . 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 1591	. . . . . . . . . . . 12 |- (w = v -> (y =/= w <-> y =/= v))
18		ineq2 2211	. . . . . . . . . . . . 13 |- (w = v -> (y i^i w) = (y i^i v))
19	18	eleq2d 1541	. . . . . . . . . . . 12 |- (w = v -> (z e. (y i^i w) <-> z e. (y i^i v)))
20	17, 19	anbi12d 628	. . . . . . . . . . 11 |- (w = v -> ((y =/= w /\ z e. (y i^i w)) <-> (y =/= v /\ z e. (y i^i v))))
21	20	cbvrexv 1801	. . . . . . . . . 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 1650	. . . . . . . . . 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	bitr 173	. . . . . . . . 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 185	. . . . . . . 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 1303	. . . . . . . 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	bitr4 176	. . . . . . 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 480	. . . . . 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 1308	. . . . . 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		ax-17 971	. . . . . . . . 9 |- ((y e. x /\ ph) -> A.u(y e. x /\ ph))
30	29	19.3 1031	. . . . . . . 8 |- (A.u(y e. x /\ ph) <-> (y e. x /\ ph))
31		kmlem14.1	. . . . . . . . . 10 |- (ph <-> (z e. y -> ((v e. x /\ y =/= v) /\ z e. v)))
32		elin 2207	. . . . . . . . . . . . . 14 |- (z e. (y i^i v) <-> (z e. y /\ z e. v))
33	32	baibr 686	. . . . . . . . . . . . 13 |- (z e. y -> (z e. v <-> z e. (y i^i v)))
34	33	anbi2d 616	. . . . . . . . . . . 12 |- (z e. y -> (((v e. x /\ y =/= v) /\ z e. v) <-> ((v e. x /\ y =/= v) /\ z e. (y i^i v))))
35		anass 439	. . . . . . . . . . . 12 |- (((v e. x /\ y =/= v) /\ z e. (y i^i v)) <-> (v e. x /\ (y =/= v /\ z e. (y i^i v))))
36	34, 35	syl6bb 536	. . . . . . . . . . 11 |- (z e. y -> (((v e. x /\ y =/= v) /\ z e. v) <-> (v e. x /\ (y =/= v /\ z e. (y i^i v)))))
37	36	pm5.74i 584	. . . . . . . . . 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)))))
38	31, 37	bitr 173	. . . . . . . . 9 |- (ph <-> (z e. y -> (v e. x /\ (y =/= v /\ z e. (y i^i v)))))
39	38	anbi2i 480	. . . . . . . 8 |- ((y e. x /\ ph) <-> (y e. x /\ (z e. y -> (v e. x /\ (y =/= v /\ z e. (y i^i v))))))
40	30, 39	bitr2 174	. . . . . . 7 |- ((y e. x /\ (z e. y -> (v e. x /\ (y =/= v /\ z e. (y i^i v))))) <-> A.u(y e. x /\ ph))
41	40	exbii 1051	. . . . . 6 |- (E.v(y e. x /\ (z e. y -> (v e. x /\ (y =/= v /\ z e. (y i^i v))))) <-> E.vA.u(y e. x /\ ph))
42	27, 28, 41	3bitr2 179	. . . . 5 |- ((y e. x /\ (z e. y -> E.w e. x (y =/= w /\ z e. (y i^i w)))) <-> E.vA.u(y e. x /\ ph))
43	42	albii 999	. . . 4 |- (A.z(y e. x /\ (z e. y -> E.w e. x (y =/= w /\ z e. (y i^i w)))) <-> A.zE.vA.u(y e. x /\ ph))
44	15, 16, 43	3bitr2 179	. . 3 |- ((y e. x /\ A.v e. y E.w e. x (y =/= w /\ v e. (y i^i w))) <-> A.zE.vA.u(y e. x /\ ph))
45	44	exbii 1051	. 2 |- (E.y(y e. x /\ A.v e. y E.w e. x (y =/= w /\ v e. (y i^i w))) <-> E.yA.zE.vA.u(y e. x /\ ph))
46	7, 8, 45	3bitr 177	1 |- (E.z e. x A.v e. z E.w e. x (z =/= w /\ v e. (z i^i w)) <-> E.yA.zE.vA.u(y e. x /\ ph))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  E.wex 980  E!weu 1380   =/= wne 1585  A.wral 1645  E.wrex 1646   i^i cin 2046

This theorem is referenced by:  kmlem16 4780

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8