Theorem kmlem1 8972

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2. (Contributed by NM, 5-Apr-2004.)

Assertion

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

Distinct variable groups:   x, y, ph   ps, x   x, w, y, z

Allowed substitution hints:   ph( z, w)   ps( y, z, w)

Proof of Theorem kmlem1

Dummy variables v u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3203	. . . . . 6 |- v e. _V
2	1	rabex 4813	. . . . 5 |- { u e. v | u =/= (/) } e. _V
3		raleq 3138	. . . . . . 7 |- ( x = { u e. v | u =/= (/) } -> ( A. z e. x z =/= (/) <-> A. z e. { u e. v | u =/= (/) } z =/= (/) ) )
4		raleq 3138	. . . . . . . 8 |- ( x = { u e. v | u =/= (/) } -> ( A. w e. x ph <-> A. w e. { u e. v | u =/= (/) } ph ) )
5	4	raleqbi1dv 3146	. . . . . . 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 747	. . . . . 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 3138	. . . . . . 7 |- ( x = { u e. v | u =/= (/) } -> ( A. z e. x ps <-> A. z e. { u e. v | u =/= (/) } ps ) )
8	7	exbidv 1850	. . . . . 6 |- ( x = { u e. v | u =/= (/) } -> ( E. y A. z e. x ps <-> E. y A. z e. { u e. v | u =/= (/) } ps ) )
9	6, 8	imbi12d 334	. . . . 5 |- ( x = { u e. v | u =/= (/) } -> ( ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. 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. y A. z e. { u e. v | u =/= (/) } ps ) ) )
10	2, 9	spcv 3299	. . . 4 |- ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. 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. y A. z e. { u e. v | u =/= (/) } ps ) )
11	10	alrimiv 1855	. . 3 |- ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. 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. y A. z e. { u e. v | u =/= (/) } ps ) )
12		elrabi 3359	. . . . . . 7 |- ( z e. { u e. v | u =/= (/) } -> z e. v )
13		elrabi 3359	. . . . . . . . 9 |- ( w e. { u e. v | u =/= (/) } -> w e. v )
14	13	imim1i 63	. . . . . . . 8 |- ( ( w e. v -> ph ) -> ( w e. { u e. v | u =/= (/) } -> ph ) )
15	14	ralimi2 2949	. . . . . . 7 |- ( A. w e. v ph -> A. w e. { u e. v | u =/= (/) } ph )
16	12, 15	imim12i 62	. . . . . 6 |- ( ( z e. v -> A. w e. v ph ) -> ( z e. { u e. v | u =/= (/) } -> A. w e. { u e. v | u =/= (/) } ph ) )
17	16	ralimi2 2949	. . . . 5 |- ( A. z e. v A. w e. v ph -> A. z e. { u e. v | u =/= (/) } A. w e. { u e. v | u =/= (/) } ph )
18		neeq1 2856	. . . . . . . 8 |- ( u = z -> ( u =/= (/) <-> z =/= (/) ) )
19	18	elrab 3363	. . . . . . 7 |- ( z e. { u e. v | u =/= (/) } <-> ( z e. v /\ z =/= (/) ) )
20	19	simprbi 480	. . . . . 6 |- ( z e. { u e. v | u =/= (/) } -> z =/= (/) )
21	20	rgen 2922	. . . . 5 |- A. z e. { u e. v | u =/= (/) } z =/= (/)
22	17, 21	jctil 560	. . . 4 |- ( 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 ) )
23	19	biimpri 218	. . . . . . . 8 |- ( ( z e. v /\ z =/= (/) ) -> z e. { u e. v | u =/= (/) } )
24	23	imim1i 63	. . . . . . 7 |- ( ( z e. { u e. v | u =/= (/) } -> ps ) -> ( ( z e. v /\ z =/= (/) ) -> ps ) )
25	24	expd 452	. . . . . 6 |- ( ( z e. { u e. v | u =/= (/) } -> ps ) -> ( z e. v -> ( z =/= (/) -> ps ) ) )
26	25	ralimi2 2949	. . . . 5 |- ( A. z e. { u e. v | u =/= (/) } ps -> A. z e. v ( z =/= (/) -> ps ) )
27	26	eximi 1762	. . . 4 |- ( E. y A. z e. { u e. v | u =/= (/) } ps -> E. y A. z e. v ( z =/= (/) -> ps ) )
28	22, 27	imim12i 62	. . 3 |- ( ( ( A. z e. { u e. v | u =/= (/) } z =/= (/) /\ A. z e. { u e. v | u =/= (/) } A. w e. { u e. v | u =/= (/) } ph ) -> E. y A. z e. { u e. v | u =/= (/) } ps ) -> ( A. z e. v A. w e. v ph -> E. y A. z e. v ( z =/= (/) -> ps ) ) )
29	11, 28	sylg 1750	. 2 |- ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. z e. x ps ) -> A. v ( A. z e. v A. w e. v ph -> E. y A. z e. v ( z =/= (/) -> ps ) ) )
30		raleq 3138	. . . . 5 |- ( v = x -> ( A. w e. v ph <-> A. w e. x ph ) )
31	30	raleqbi1dv 3146	. . . 4 |- ( v = x -> ( A. z e. v A. w e. v ph <-> A. z e. x A. w e. x ph ) )
32		raleq 3138	. . . . 5 |- ( v = x -> ( A. z e. v ( z =/= (/) -> ps ) <-> A. z e. x ( z =/= (/) -> ps ) ) )
33	32	exbidv 1850	. . . 4 |- ( v = x -> ( E. y A. z e. v ( z =/= (/) -> ps ) <-> E. y A. z e. x ( z =/= (/) -> ps ) ) )
34	31, 33	imbi12d 334	. . 3 |- ( v = x -> ( ( A. z e. v A. w e. v ph -> E. y A. z e. v ( z =/= (/) -> ps ) ) <-> ( A. z e. x A. w e. x ph -> E. y A. z e. x ( z =/= (/) -> ps ) ) ) )
35	34	cbvalv 2273	. 2 |- ( A. v ( A. z e. v A. w e. v ph -> E. y A. z e. v ( z =/= (/) -> ps ) ) <-> A. x ( A. z e. x A. w e. x ph -> E. y A. z e. x ( z =/= (/) -> ps ) ) )
36	29, 35	sylib 208	1 |- ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ph ) -> E. y A. z e. x ps ) -> A. x ( A. z e. x A. w e. x ph -> E. y A. z e. x ( z =/= (/) -> ps ) ) )

Syntax hints:   -> wi 4   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   {crab 2916   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rab 2921  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  kmlem13  8984