Theorem kmlem1 3580

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

Assertion

Ref	Expression
kmlem1	|- (A.x((A.z e. x -. z = (/) /\ A.z e. x A.w e. x ph) -> E.yA.z e. x ps) -> A.x(A.z e. x A.w e. x ph -> E.yA.z e. x (-. z = (/) -> ps)))

Distinct variable group(s):   x,y,z,w   ph,x,y   ps,x

Proof of Theorem kmlem1

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . 6 |- v e. V
2	1	rabex 1706	. . . . 5 |- {u e. v | -. u = (/)} e. V
3		raleq 1324	. . . . . . 7 |- (x = {u e. v | -. u = (/)} -> (A.z e. x -. z = (/) <-> A.z e. {u e. v | -. u = (/)} -. z = (/)))
4		raleq 1324	. . . . . . . 8 |- (x = {u e. v | -. u = (/)} -> (A.w e. x ph <-> A.w e. {u e. v | -. u = (/)}ph))
5	4	raleqd 1327	. . . . . . 7 |- (x = {u e. v | -. u = (/)} -> (A.z e. x A.w e. x ph <-> A.z e. {u e. v | -. u = (/)}A.w e. {u e. v | -. u = (/)}ph))
6	3, 5	anbi12d 476	. . . . . 6 |- (x = {u e. v | -. u = (/)} -> ((A.z e. x -. z = (/) /\ A.z e. x A.w e. x ph) <-> (A.z e. {u e. v | -. u = (/)} -. z = (/) /\ A.z e. {u e. v | -. u = (/)}A.w e. {u e. v | -. u = (/)}ph)))
7		raleq 1324	. . . . . . 7 |- (x = {u e. v | -. u = (/)} -> (A.z e. x ps <-> A.z e. {u e. v | -. u = (/)}ps))
8	7	biexdv 936	. . . . . 6 |- (x = {u e. v | -. u = (/)} -> (E.yA.z e. x ps <-> E.yA.z e. {u e. v | -. u = (/)}ps))
9	6, 8	imbi12d 474	. . . . 5 |- (x = {u e. v | -. u = (/)} -> (((A.z e. x -. z = (/) /\ A.z e. x A.w e. x ph) -> E.yA.z e. x ps) <-> ((A.z e. {u e. v | -. u = (/)} -. z = (/) /\ A.z e. {u e. v | -. u = (/)}A.w e. {u e. v | -. u = (/)}ph) -> E.yA.z e. {u e. v | -. u = (/)}ps)))
10	2, 9	cla4v 1400	. . . 4 |- (A.x((A.z e. x -. z = (/) /\ A.z e. x A.w e. x ph) -> E.yA.z e. x ps) -> ((A.z e. {u e. v | -. u = (/)} -. z = (/) /\ A.z e. {u e. v | -. u = (/)}A.w e. {u e. v | -. u = (/)}ph) -> E.yA.z e. {u e. v | -. u = (/)}ps))
11	10	19.21aiv 943	. . 3 |- (A.x((A.z e. x -. z = (/) /\ A.z e. x A.w e. x ph) -> E.yA.z e. x ps) -> A.v((A.z e. {u e. v | -. u = (/)} -. z = (/) /\ A.z e. {u e. v | -. u = (/)}A.w e. {u e. v | -. u = (/)}ph) -> E.yA.z e. {u e. v | -. u = (/)}ps))
12		ssrab 1556	. . . . . . . . 9 |- {u e. v | -. u = (/)} (_ v
13	12	sseli 1504	. . . . . . . 8 |- (z e. {u e. v | -. u = (/)} -> z e. v)
14	12	sseli 1504	. . . . . . . . . 10 |- (w e. {u e. v | -. u = (/)} -> w e. v)
15	14	syl4 19	. . . . . . . . 9 |- ((w e. v -> ph) -> (w e. {u e. v | -. u = (/)} -> ph))
16	15	r19.20i2 1252	. . . . . . . 8 |- (A.w e. v ph -> A.w e. {u e. v | -. u = (/)}ph)
17	13, 16	syl34 20	. . . . . . 7 |- ((z e. v -> A.w e. v ph) -> (z e. {u e. v | -. u = (/)} -> A.w e. {u e. v | -. u = (/)}ph))
18	17	r19.20i2 1252	. . . . . 6 |- (A.z e. v A.w e. v ph -> A.z e. {u e. v | -. u = (/)}A.w e. {u e. v | -. u = (/)}ph)
19		cleq1 1107	. . . . . . . . . 10 |- (u = z -> (u = (/) <-> z = (/)))
20	19	negbid 463	. . . . . . . . 9 |- (u = z -> (-. u = (/) <-> -. z = (/)))
21	20	elrab 1422	. . . . . . . 8 |- (z e. {u e. v | -. u = (/)} <-> (z e. v /\ -. z = (/)))
22	21	pm3.27bd 263	. . . . . . 7 |- (z e. {u e. v | -. u = (/)} -> -. z = (/))
23	22	rgen 1247	. . . . . 6 |- A.z e. {u e. v | -. u = (/)} -. z = (/)
24	18, 23	jctil 240	. . . . 5 |- (A.z e. v A.w e. v ph -> (A.z e. {u e. v | -. u = (/)} -. z = (/) /\ A.z e. {u e. v | -. u = (/)}A.w e. {u e. v | -. u = (/)}ph))
25	21	biimpr 134	. . . . . . . . 9 |- ((z e. v /\ -. z = (/)) -> z e. {u e. v | -. u = (/)})
26	25	syl4 19	. . . . . . . 8 |- ((z e. {u e. v | -. u = (/)} -> ps) -> ((z e. v /\ -. z = (/)) -> ps))
27	26	exp3a 292	. . . . . . 7 |- ((z e. {u e. v | -. u = (/)} -> ps) -> (z e. v -> (-. z = (/) -> ps)))
28	27	r19.20i2 1252	. . . . . 6 |- (A.z e. {u e. v | -. u = (/)}ps -> A.z e. v (-. z = (/) -> ps))
29	28	19.22i 723	. . . . 5 |- (E.yA.z e. {u e. v | -. u = (/)}ps -> E.yA.z e. v (-. z = (/) -> ps))
30	24, 29	syl34 20	. . . 4 |- (((A.z e. {u e. v | -. u = (/)} -. z = (/) /\ A.z e. {u e. v | -. u = (/)}A.w e. {u e. v | -. u = (/)}ph) -> E.yA.z e. {u e. v | -. u = (/)}ps) -> (A.z e. v A.w e. v ph -> E.yA.z e. v (-. z = (/) -> ps)))
31	30	19.20i 691	. . 3 |- (A.v((A.z e. {u e. v | -. u = (/)} -. z = (/) /\ A.z e. {u e. v | -. u = (/)}A.w e. {u e. v | -. u = (/)}ph) -> E.yA.z e. {u e. v | -. u = (/)}ps) -> A.v(A.z e. v A.w e. v ph -> E.yA.z e. v (-. z = (/) -> ps)))
32	11, 31	syl 12	. 2 |- (A.x((A.z e. x -. z = (/) /\ A.z e. x A.w e. x ph) -> E.yA.z e. x ps) -> A.v(A.z e. v A.w e. v ph -> E.yA.z e. v (-. z = (/) -> ps)))
33		raleq 1324	. . . . 5 |- (v = x -> (A.w e. v ph <-> A.w e. x ph))
34	33	raleqd 1327	. . . 4 |- (v = x -> (A.z e. v A.w e. v ph <-> A.z e. x A.w e. x ph))
35		raleq 1324	. . . . 5 |- (v = x -> (A.z e. v (-. z = (/) -> ps) <-> A.z e. x (-. z = (/) -> ps)))
36	35	biexdv 936	. . . 4 |- (v = x -> (E.yA.z e. v (-. z = (/) -> ps) <-> E.yA.z e. x (-. z = (/) -> ps)))
37	34, 36	imbi12d 474	. . 3 |- (v = x -> ((A.z e. v A.w e. v ph -> E.yA.z e. v (-. z = (/) -> ps)) <-> (A.z e. x A.w e. x ph -> E.yA.z e. x (-. z = (/) -> ps))))
38	37	cbvalv 972	. 2 |- (A.v(A.z e. v A.w e. v ph -> E.yA.z e. v (-. z = (/) -> ps)) <-> A.x(A.z e. x A.w e. x ph -> E.yA.z e. x (-. z = (/) -> ps)))
39	32, 38	sylib 173	1 |- (A.x((A.z e. x -. z = (/) /\ A.z e. x A.w e. x ph) -> E.yA.z e. x ps) -> A.x(A.z e. x A.w e. x ph -> E.yA.z e. x (-. z = (/) -> ps)))

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196  A.wal 672  E.wex 678   = weq 797   e. wel 803   = wceq 1091   e. wcel 1092  A.wral 1201  {crab 1204  (/)c0 1707

This theorem is referenced by:  kmlem12 3591

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-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rab 1208  df-v 1349  df-in 1491  df-ss 1492

metamath.org