Theorem kmlem4 3583

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

Assertion

Ref	Expression
kmlem4	|- ((w e. x /\ -. z = w) -> ((z \ U.(x \ {z})) i^i w) = (/))

Proof of Theorem kmlem4

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . 6 |- w e. V
2		eleq1 1149	. . . . . . . 8 |- (v = w -> (v e. x <-> w e. x))
3		cleq2 1110	. . . . . . . . 9 |- (v = w -> (z = v <-> z = w))
4	3	negbid 463	. . . . . . . 8 |- (v = w -> (-. z = v <-> -. z = w))
5	2, 4	anbi12d 476	. . . . . . 7 |- (v = w -> ((v e. x /\ -. z = v) <-> (w e. x /\ -. z = w)))
6		eleq2 1150	. . . . . . . 8 |- (v = w -> (y e. v <-> y e. w))
7	6	negbid 463	. . . . . . 7 |- (v = w -> (-. y e. v <-> -. y e. w))
8	5, 7	imbi12d 474	. . . . . 6 |- (v = w -> (((v e. x /\ -. z = v) -> -. y e. v) <-> ((w e. x /\ -. z = w) -> -. y e. w)))
9	1, 8	cla4v 1400	. . . . 5 |- (A.v((v e. x /\ -. z = v) -> -. y e. v) -> ((w e. x /\ -. z = w) -> -. y e. w))
10	9	com12 13	. . . 4 |- ((w e. x /\ -. z = w) -> (A.v((v e. x /\ -. z = v) -> -. y e. v) -> -. y e. w))
11		eldif 1496	. . . . 5 |- (y e. (z \ U.(x \ {z})) <-> (y e. z /\ -. y e. U.(x \ {z})))
12		pm3.27 260	. . . . . 6 |- ((y e. z /\ -. y e. U.(x \ {z})) -> -. y e. U.(x \ {z}))
13		eluni 1922	. . . . . . . 8 |- (y e. U.(x \ {z}) <-> E.v(y e. v /\ v e. (x \ {z})))
14	13	negbii 162	. . . . . . 7 |- (-. y e. U.(x \ {z}) <-> -. E.v(y e. v /\ v e. (x \ {z})))
15		alnex 716	. . . . . . . 8 |- (A.v -. (y e. v /\ v e. (x \ {z})) <-> -. E.v(y e. v /\ v e. (x \ {z})))
16		ianor 253	. . . . . . . . . 10 |- (-. (y e. v /\ v e. (x \ {z})) <-> (-. y e. v \/ -. v e. (x \ {z})))
17		eldif 1496	. . . . . . . . . . . . . . 15 |- (v e. (x \ {z}) <-> (v e. x /\ -. v e. {z}))
18		elsn 1820	. . . . . . . . . . . . . . . . . 18 |- (v e. {z} <-> v = z)
19		cleqcom 1103	. . . . . . . . . . . . . . . . . 18 |- (v = z <-> z = v)
20	18, 19	bitr 151	. . . . . . . . . . . . . . . . 17 |- (v e. {z} <-> z = v)
21	20	negbii 162	. . . . . . . . . . . . . . . 16 |- (-. v e. {z} <-> -. z = v)
22	21	anbi2i 367	. . . . . . . . . . . . . . 15 |- ((v e. x /\ -. v e. {z}) <-> (v e. x /\ -. z = v))
23	17, 22	bitr 151	. . . . . . . . . . . . . 14 |- (v e. (x \ {z}) <-> (v e. x /\ -. z = v))
24	23	negbii 162	. . . . . . . . . . . . 13 |- (-. v e. (x \ {z}) <-> -. (v e. x /\ -. z = v))
25		iman 205	. . . . . . . . . . . . 13 |- ((v e. x -> z = v) <-> -. (v e. x /\ -. z = v))
26	24, 25	bitr4 154	. . . . . . . . . . . 12 |- (-. v e. (x \ {z}) <-> (v e. x -> z = v))
27	26	imbi2i 160	. . . . . . . . . . 11 |- ((y e. v -> -. v e. (x \ {z})) <-> (y e. v -> (v e. x -> z = v)))
28		imor 204	. . . . . . . . . . 11 |- ((y e. v -> -. v e. (x \ {z})) <-> (-. y e. v \/ -. v e. (x \ {z})))
29		pm4.1 143	. . . . . . . . . . . . 13 |- ((y e. v -> z = v) <-> (-. z = v -> -. y e. v))
30	29	imbi2i 160	. . . . . . . . . . . 12 |- ((v e. x -> (y e. v -> z = v)) <-> (v e. x -> (-. z = v -> -. y e. v)))
31		bi2.04 141	. . . . . . . . . . . 12 |- ((y e. v -> (v e. x -> z = v)) <-> (v e. x -> (y e. v -> z = v)))
32		impexp 276	. . . . . . . . . . . 12 |- (((v e. x /\ -. z = v) -> -. y e. v) <-> (v e. x -> (-. z = v -> -. y e. v)))
33	30, 31, 32	3bitr4 158	. . . . . . . . . . 11 |- ((y e. v -> (v e. x -> z = v)) <-> ((v e. x /\ -. z = v) -> -. y e. v))
34	27, 28, 33	3bitr3 156	. . . . . . . . . 10 |- ((-. y e. v \/ -. v e. (x \ {z})) <-> ((v e. x /\ -. z = v) -> -. y e. v))
35	16, 34	bitr 151	. . . . . . . . 9 |- (-. (y e. v /\ v e. (x \ {z})) <-> ((v e. x /\ -. z = v) -> -. y e. v))
36	35	bial 695	. . . . . . . 8 |- (A.v -. (y e. v /\ v e. (x \ {z})) <-> A.v((v e. x /\ -. z = v) -> -. y e. v))
37	15, 36	bitr3 153	. . . . . . 7 |- (-. E.v(y e. v /\ v e. (x \ {z})) <-> A.v((v e. x /\ -. z = v) -> -. y e. v))
38	14, 37	bitr 151	. . . . . 6 |- (-. y e. U.(x \ {z}) <-> A.v((v e. x /\ -. z = v) -> -. y e. v))
39	12, 38	sylib 173	. . . . 5 |- ((y e. z /\ -. y e. U.(x \ {z})) -> A.v((v e. x /\ -. z = v) -> -. y e. v))
40	11, 39	sylbi 174	. . . 4 |- (y e. (z \ U.(x \ {z})) -> A.v((v e. x /\ -. z = v) -> -. y e. v))
41	10, 40	syl5 22	. . 3 |- ((w e. x /\ -. z = w) -> (y e. (z \ U.(x \ {z})) -> -. y e. w))
42	41	r19.21aiv 1259	. 2 |- ((w e. x /\ -. z = w) -> A.y e. (z \ U.(x \ {z})) -. y e. w)
43		disj 1733	. 2 |- (((z \ U.(x \ {z})) i^i w) = (/) <-> A.y e. (z \ U.(x \ {z})) -. y e. w)
44	42, 43	sylibr 175	1 |- ((w e. x /\ -. z = w) -> ((z \ U.(x \ {z})) i^i w) = (/))

Syntax hints:  -. wn 1   -> wi 2   \/ wo 195   /\ wa 196  A.wal 672  E.wex 678   = weq 797   e. wel 803   = wceq 1091   e. wcel 1092  A.wral 1201   \ cdif 1484   i^i cin 1486  (/)c0 1707  {csn 1808  U.cuni 1919

This theorem is referenced by:  kmlem5 3584  kmlem10 3589

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-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-v 1349  df-dif 1489  df-in 1491  df-nul 1708  df-sn 1811  df-uni 1920

metamath.org