Theorem kmlem15 4751

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 groups:   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 968	. . . . . . 7 |- (v e. (z i^i y) -> A.u v e. (z i^i y))
3	2	eu1 1385	. . . . . 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 2197	. . . . . . . . 9 |- (v e. (z i^i y) <-> (v e. z /\ v e. y))
5		ax-17 968	. . . . . . . . . . . . 13 |- (u e. (z i^i y) -> A.v u e. (z i^i y))
6		eleq1 1526	. . . . . . . . . . . . 13 |- (v = u -> (v e. (z i^i y) <-> u e. (z i^i y)))
7	5, 6	sbie 1192	. . . . . . . . . . . 12 |- ([u / v]v e. (z i^i y) <-> u e. (z i^i y))
8		elin 2197	. . . . . . . . . . . 12 |- (u e. (z i^i y) <-> (u e. z /\ u e. y))
9	7, 8	bitr 173	. . . . . . . . . . 11 |- ([u / v]v e. (z i^i y) <-> (u e. z /\ u e. y))
10		eqcom 1469	. . . . . . . . . . 11 |- (v = u <-> u = v)
11	9, 10	imbi12i 188	. . . . . . . . . 10 |- (([u / v]v e. (z i^i y) -> v = u) <-> ((u e. z /\ u e. y) -> u = v))
12	11	albii 996	. . . . . . . . 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 481	. . . . . . . 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 1294	. . . . . . . 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 176	. . . . . . 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	exbii 1047	. . . . . 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 173	. . . . 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	ralbii 1659	. . . 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 1641	. . . . 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	albii 996	. . . . . . . . 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 1280	. . . . . . . . 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 173	. . . . . . . 8 |- (A.ups <-> (z e. x -> A.u((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))
24	23	exbii 1047	. . . . . . 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 1298	. . . . . . 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 173	. . . . . 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	albii 996	. . . . 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 176	. . . 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 177	. . 3 |- (ch <-> A.zE.vA.ups)
30	29	anbi2i 479	. 2 |- ((-. y e. x /\ ch) <-> (-. y e. x /\ A.zE.vA.ups))
31		19.28v 1294	. 2 |- (A.z(-. y e. x /\ E.vA.ups) <-> (-. y e. x /\ A.zE.vA.ups))
32		19.28v 1294	. . . . 5 |- (A.u(-. y e. x /\ ps) <-> (-. y e. x /\ A.ups))
33	32	exbii 1047	. . . 4 |- (E.vA.u(-. y e. x /\ ps) <-> E.v(-. y e. x /\ A.ups))
34		19.42v 1303	. . . 4 |- (E.v(-. y e. x /\ A.ups) <-> (-. y e. x /\ E.vA.ups))
35	33, 34	bitr2 174	. . 3 |- ((-. y e. x /\ E.vA.ups) <-> E.vA.u(-. y e. x /\ ps))
36	35	albii 996	. 2 |- (A.z(-. y e. x /\ E.vA.ups) <-> A.zE.vA.u(-. y e. x /\ ps))
37	30, 31, 36	3bitr2 179	1 |- ((-. y e. x /\ ch) <-> A.zE.vA.u(-. y e. x /\ ps))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955  E.wex 977  [wsbc 1166  E!weu 1373   =/= wne 1577  A.wral 1637   i^i cin 2036

This theorem is referenced by:  kmlem16 4752

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-clab 1457  df-cleq 1462  df-clel 1465  df-ral 1641  df-v 1803  df-in 2041

Copyright terms: Public domain