Theorem kmlem15 3594

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
kmlem15	|- ((-. y e. x /\ ch) <-> A.zE.vA.u(-. y e. x /\ ps))

Distinct variable group(s):   x,y,z,v,u   ph,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		ax-17 925	. . . . . . 7 |- (v e. (z i^i y) -> A.u v e. (z i^i y))
3	2	eu1 1019	. . . . . 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 1635	. . . . . . . . 9 |- (v e. (z i^i y) <-> (v e. z /\ v e. y))
5		ax-17 925	. . . . . . . . . . . . 13 |- (u e. (z i^i y) -> A.v u e. (z i^i y))
6		eleq1 1149	. . . . . . . . . . . . 13 |- (v = u -> (v e. (z i^i y) <-> u e. (z i^i y)))
7	5, 6	sbie 904	. . . . . . . . . . . 12 |- ([u / v]v e. (z i^i y) <-> u e. (z i^i y))
8		elin 1635	. . . . . . . . . . . 12 |- (u e. (z i^i y) <-> (u e. z /\ u e. y))
9	7, 8	bitr 151	. . . . . . . . . . 11 |- ([u / v]v e. (z i^i y) <-> (u e. z /\ u e. y))
10		cleqcom 1103	. . . . . . . . . . 11 |- (v = u <-> u = v)
11	9, 10	imbi12i 163	. . . . . . . . . 10 |- (([u / v]v e. (z i^i y) -> v = u) <-> ((u e. z /\ u e. y) -> u = v))
12	11	bial 695	. . . . . . . . 9 |- (A.u([u / v]v e. (z i^i y) -> v = u) <-> A.u((u e. z /\ u e. y) -> u = v))
13	4, 12	anbi12i 369	. . . . . . . 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)))
14		19.28v 957	. . . . . . . 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)))
15	13, 14	bitr4 154	. . . . . . 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)))
16	15	biex 733	. . . . . 6 |- (E.v(v e. (z i^i y) /\ A.u([u / v]v e. (z i^i y) -> v = u)) <-> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)))
17	3, 16	bitr 151	. . . . 5 |- (E!v v e. (z i^i y) <-> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)))
18	17	biral 1223	. . . 4 |- (A.z e. x E!v v e. (z i^i y) <-> A.z e. x E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)))
19		df-ral 1205	. . . . 5 |- (A.z e. x E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)) <-> A.z(z e. x -> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
20		kmlem14.2	. . . . . . . . . 10 |- (ps <-> (z e. x -> ((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
21	20	bial 695	. . . . . . . . 9 |- (A.ups <-> A.u(z e. x -> ((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
22		19.21v 942	. . . . . . . . 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))))
23	21, 22	bitr 151	. . . . . . . 8 |- (A.ups <-> (z e. x -> A.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
24	23	biex 733	. . . . . . 7 |- (E.vA.ups <-> E.v(z e. x -> A.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
25		19.37v 961	. . . . . . 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.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
26	24, 25	bitr 151	. . . . . 6 |- (E.vA.ups <-> (z e. x -> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
27	26	bial 695	. . . . 5 |- (A.zE.vA.ups <-> A.z(z e. x -> E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
28	19, 27	bitr4 154	. . . 4 |- (A.z e. x E.vA.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)) <-> A.zE.vA.ups)
29	1, 18, 28	3bitr 155	. . 3 |- (ch <-> A.zE.vA.ups)
30	29	anbi2i 367	. 2 |- ((-. y e. x /\ ch) <-> (-. y e. x /\ A.zE.vA.ups))
31		19.28v 957	. . 3 |- (A.z(-. y e. x /\ E.vA.ups) <-> (-. y e. x /\ A.zE.vA.ups))
32		19.28v 957	. . . . . 6 |- (A.u(-. y e. x /\ ps) <-> (-. y e. x /\ A.ups))
33	32	biex 733	. . . . 5 |- (E.vA.u(-. y e. x /\ ps) <-> E.v(-. y e. x /\ A.ups))
34		19.42v 966	. . . . 5 |- (E.v(-. y e. x /\ A.ups) <-> (-. y e. x /\ E.vA.ups))
35	33, 34	bitr2 152	. . . 4 |- ((-. y e. x /\ E.vA.ups) <-> E.vA.u(-. y e. x /\ ps))
36	35	bial 695	. . 3 |- (A.z(-. y e. x /\ E.vA.ups) <-> A.zE.vA.u(-. y e. x /\ ps))
37	31, 36	bitr3 153	. 2 |- ((-. y e. x /\ A.zE.vA.ups) <-> A.zE.vA.u(-. y e. x /\ ps))
38	30, 37	bitr 151	1 |- ((-. y e. x /\ ch) <-> A.zE.vA.u(-. y e. x /\ ps))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672  E.wex 678   = weq 797   e. wel 803  [wsb 852  E!weu 1007   e. wcel 1092  A.wral 1201   i^i cin 1486

This theorem is referenced by:  kmlem16 3595

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-v 1349  df-in 1491

metamath.org