Theorem kmlem14 3593

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 group(s):   x,y,z,w,v,u   ph,u

Proof of Theorem kmlem14

Step	Hyp	Ref	Expression
1		cleq1 1107	. . . . . . 7 |- (z = y -> (z = w <-> y = w))
2	1	negbid 463	. . . . . 6 |- (z = y -> (-. z = w <-> -. y = w))
3		ineq1 1638	. . . . . . 7 |- (z = y -> (z i^i w) = (y i^i w))
4	3	eleq2d 1156	. . . . . 6 |- (z = y -> (v e. (z i^i w) <-> v e. (y i^i w)))
5	2, 4	anbi12d 476	. . . . 5 |- (z = y -> ((-. z = w /\ v e. (z i^i w)) <-> (-. y = w /\ v e. (y i^i w))))
6	5	birexdv 1220	. . . 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))))
7	6	raleqd 1327	. . 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))))
8	7	cbvrexv 1334	. 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)))
9		df-rex 1206	. 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))))
10		eleq1 1149	. . . . . . . . 9 |- (v = z -> (v e. (y i^i w) <-> z e. (y i^i w)))
11	10	anbi2d 468	. . . . . . . 8 |- (v = z -> ((-. y = w /\ v e. (y i^i w)) <-> (-. y = w /\ z e. (y i^i w))))
12	11	birexdv 1220	. . . . . . 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))))
13	12	cbvralv 1333	. . . . . 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)))
14		df-ral 1205	. . . . . 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))))
15	13, 14	bitr 151	. . . . 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))))
16	15	anbi2i 367	. . . 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)))))
17		19.28v 957	. . . . 5 |- (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)))))
18		cleq2 1110	. . . . . . . . . . . . . 14 |- (w = v -> (y = w <-> y = v))
19	18	negbid 463	. . . . . . . . . . . . 13 |- (w = v -> (-. y = w <-> -. y = v))
20		ineq2 1639	. . . . . . . . . . . . . 14 |- (w = v -> (y i^i w) = (y i^i v))
21	20	eleq2d 1156	. . . . . . . . . . . . 13 |- (w = v -> (z e. (y i^i w) <-> z e. (y i^i v)))
22	19, 21	anbi12d 476	. . . . . . . . . . . 12 |- (w = v -> ((-. y = w /\ z e. (y i^i w)) <-> (-. y = v /\ z e. (y i^i v))))
23	22	cbvrexv 1334	. . . . . . . . . . 11 |- (E.w e. x (-. y = w /\ z e. (y i^i w)) <-> E.v e. x (-. y = v /\ z e. (y i^i v)))
24		df-rex 1206	. . . . . . . . . . 11 |- (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))))
25	23, 24	bitr 151	. . . . . . . . . 10 |- (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))))
26	25	imbi2i 160	. . . . . . . . 9 |- ((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)))))
27		19.37v 961	. . . . . . . . 9 |- (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)))))
28	26, 27	bitr4 154	. . . . . . . 8 |- ((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)))))
29	28	anbi2i 367	. . . . . . 7 |- ((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))))))
30		19.42v 966	. . . . . . . 8 |- (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))))))
31		kmlem14.1	. . . . . . . . . . . 12 |- (ph <-> (z e. y -> ((v e. x /\ -. y = v) /\ z e. v)))
32		elin 1635	. . . . . . . . . . . . . . . 16 |- (z e. (y i^i v) <-> (z e. y /\ z e. v))
33	32	baibr 507	. . . . . . . . . . . . . . 15 |- (z e. y -> (z e. v <-> z e. (y i^i v)))
34	33	anbi2d 468	. . . . . . . . . . . . . 14 |- (z e. y -> (((v e. x /\ -. y = v) /\ z e. v) <-> ((v e. x /\ -. y = v) /\ z e. (y i^i v))))
35		anass 336	. . . . . . . . . . . . . 14 |- (((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 414	. . . . . . . . . . . . 13 |- (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 443	. . . . . . . . . . . 12 |- ((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 151	. . . . . . . . . . 11 |- (ph <-> (z e. y -> (v e. x /\ (-. y = v /\ z e. (y i^i v)))))
39	38	anbi2i 367	. . . . . . . . . 10 |- ((y e. x /\ ph) <-> (y e. x /\ (z e. y -> (v e. x /\ (-. y = v /\ z e. (y i^i v))))))
40		ax-17 925	. . . . . . . . . . 11 |- ((y e. x /\ ph) -> A.u(y e. x /\ ph))
41	40	19.3r 714	. . . . . . . . . 10 |- ((y e. x /\ ph) <-> A.u(y e. x /\ ph))
42	39, 41	bitr3 153	. . . . . . . . 9 |- ((y e. x /\ (z e. y -> (v e. x /\ (-. y = v /\ z e. (y i^i v))))) <-> A.u(y e. x /\ ph))
43	42	biex 733	. . . . . . . 8 |- (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))
44	30, 43	bitr3 153	. . . . . . 7 |- ((y e. x /\ E.v(z e. y -> (v e. x /\ (-. y = v /\ z e. (y i^i v))))) <-> E.vA.u(y e. x /\ ph))
45	29, 44	bitr 151	. . . . . 6 |- ((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))
46	45	bial 695	. . . . 5 |- (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))
47	17, 46	bitr3 153	. . . 4 |- ((y e. x /\ A.z(z e. y -> E.w e. x (-. y = w /\ z e. (y i^i w)))) <-> A.zE.vA.u(y e. x /\ ph))
48	16, 47	bitr 151	. . 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)