Theorem kmlem3 8974

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. The right-hand side is part of the hypothesis of 4. (Contributed by NM, 25-Mar-2004.)

Assertion

Ref	Expression
kmlem3	|- ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )

Distinct variable group:   x, v, w, z

Proof of Theorem kmlem3

Step	Hyp	Ref	Expression
1		dfdif2 3583	. . . 4 |- ( z \ U. ( x \ { z } ) ) = { v e. z | -. v e. U. ( x \ { z } ) }
2		dfnul3 3918	. . . . . 6 |- (/) = { v e. z | -. v e. z }
3	2	uneq2i 3764	. . . . 5 |- ( { v e. z | -. v e. U. ( x \ { z } ) } u. (/) ) = ( { v e. z | -. v e. U. ( x \ { z } ) } u. { v e. z | -. v e. z } )
4		un0 3967	. . . . 5 |- ( { v e. z | -. v e. U. ( x \ { z } ) } u. (/) ) = { v e. z | -. v e. U. ( x \ { z } ) }
5		unrab 3898	. . . . 5 |- ( { v e. z | -. v e. U. ( x \ { z } ) } u. { v e. z | -. v e. z } ) = { v e. z | ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) }
6	3, 4, 5	3eqtr3i 2652	. . . 4 |- { v e. z | -. v e. U. ( x \ { z } ) } = { v e. z | ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) }
7		ianor 509	. . . . . . 7 |- ( -. ( v e. U. ( x \ { z } ) /\ v e. z ) <-> ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) )
8		eluni 4439	. . . . . . . . . 10 |- ( v e. U. ( x \ { z } ) <-> E. w ( v e. w /\ w e. ( x \ { z } ) ) )
9	8	anbi1i 731	. . . . . . . . 9 |- ( ( v e. U. ( x \ { z } ) /\ v e. z ) <-> ( E. w ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
10		df-rex 2918	. . . . . . . . . 10 |- ( E. w e. x -. ( z =/= w -> -. v e. ( z i^i w ) ) <-> E. w ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) )
11		elin 3796	. . . . . . . . . . . . . . 15 |- ( v e. ( z i^i w ) <-> ( v e. z /\ v e. w ) )
12	11	anbi2i 730	. . . . . . . . . . . . . 14 |- ( ( z =/= w /\ v e. ( z i^i w ) ) <-> ( z =/= w /\ ( v e. z /\ v e. w ) ) )
13		df-an 386	. . . . . . . . . . . . . 14 |- ( ( z =/= w /\ v e. ( z i^i w ) ) <-> -. ( z =/= w -> -. v e. ( z i^i w ) ) )
14	12, 13	bitr3i 266	. . . . . . . . . . . . 13 |- ( ( z =/= w /\ ( v e. z /\ v e. w ) ) <-> -. ( z =/= w -> -. v e. ( z i^i w ) ) )
15	14	anbi2i 730	. . . . . . . . . . . 12 |- ( ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) <-> ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) )
16		eldifsn 4317	. . . . . . . . . . . . . . . 16 |- ( w e. ( x \ { z } ) <-> ( w e. x /\ w =/= z ) )
17		necom 2847	. . . . . . . . . . . . . . . . 17 |- ( w =/= z <-> z =/= w )
18	17	anbi2i 730	. . . . . . . . . . . . . . . 16 |- ( ( w e. x /\ w =/= z ) <-> ( w e. x /\ z =/= w ) )
19	16, 18	bitri 264	. . . . . . . . . . . . . . 15 |- ( w e. ( x \ { z } ) <-> ( w e. x /\ z =/= w ) )
20	19	anbi2i 730	. . . . . . . . . . . . . 14 |- ( ( ( v e. w /\ v e. z ) /\ w e. ( x \ { z } ) ) <-> ( ( v e. w /\ v e. z ) /\ ( w e. x /\ z =/= w ) ) )
21		ancom 466	. . . . . . . . . . . . . . 15 |- ( ( v e. w /\ v e. z ) <-> ( v e. z /\ v e. w ) )
22	21	anbi2ci 732	. . . . . . . . . . . . . 14 |- ( ( ( v e. w /\ v e. z ) /\ ( w e. x /\ z =/= w ) ) <-> ( ( w e. x /\ z =/= w ) /\ ( v e. z /\ v e. w ) ) )
23		anass 681	. . . . . . . . . . . . . 14 |- ( ( ( w e. x /\ z =/= w ) /\ ( v e. z /\ v e. w ) ) <-> ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) )
24	20, 22, 23	3bitri 286	. . . . . . . . . . . . 13 |- ( ( ( v e. w /\ v e. z ) /\ w e. ( x \ { z } ) ) <-> ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) )
25		an32 839	. . . . . . . . . . . . 13 |- ( ( ( v e. w /\ v e. z ) /\ w e. ( x \ { z } ) ) <-> ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
26	24, 25	bitr3i 266	. . . . . . . . . . . 12 |- ( ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) <-> ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
27	15, 26	bitr3i 266	. . . . . . . . . . 11 |- ( ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) <-> ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
28	27	exbii 1774	. . . . . . . . . 10 |- ( E. w ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) <-> E. w ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
29		19.41v 1914	. . . . . . . . . 10 |- ( E. w ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) <-> ( E. w ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
30	10, 28, 29	3bitri 286	. . . . . . . . 9 |- ( E. w e. x -. ( z =/= w -> -. v e. ( z i^i w ) ) <-> ( E. w ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
31		rexnal 2995	. . . . . . . . 9 |- ( E. w e. x -. ( z =/= w -> -. v e. ( z i^i w ) ) <-> -. A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )
32	9, 30, 31	3bitr2ri 289	. . . . . . . 8 |- ( -. A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) <-> ( v e. U. ( x \ { z } ) /\ v e. z ) )
33	32	con1bii 346	. . . . . . 7 |- ( -. ( v e. U. ( x \ { z } ) /\ v e. z ) <-> A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )
34	7, 33	bitr3i 266	. . . . . 6 |- ( ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) <-> A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )
35	34	a1i 11	. . . . 5 |- ( v e. z -> ( ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) <-> A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) ) )
36	35	rabbiia 3185	. . . 4 |- { v e. z | ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) } = { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) }
37	1, 6, 36	3eqtri 2648	. . 3 |- ( z \ U. ( x \ { z } ) ) = { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) }
38	37	neeq1i 2858	. 2 |- ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) } =/= (/) )
39		rabn0 3958	. 2 |- ( { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) } =/= (/) <-> E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )
40	38, 39	bitri 264	1 |- ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   \ cdif 3571   u. cun 3572   i^i cin 3573   (/)c0 3915   {csn 4177   U.cuni 4436

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

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-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-nul 3916  df-sn 4178  df-uni 4437

This theorem is referenced by:  kmlem13  8984