Theorem kmlem3 4739

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.

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 2046	. . . 4 |- (z \ U.(x \ {z})) = {v e. z | -. v e. U.(x \ {z})}
2		dfnul3 2273	. . . . . 6 |- (/) = {v e. z | -. v e. z}
3	2	uneq2i 2171	. . . . 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 2287	. . . . 5 |- ({v e. z | -. v e. U.(x \ {z})} u. (/)) = {v e. z | -. v e. U.(x \ {z})}
5		unrab 2260	. . . . 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	3eqtr3 1495	. . . 4 |- {v e. z | -. v e. U.(x \ {z})} = {v e. z | (-. v e. U.(x \ {z}) \/ -. v e. z)}
7		ianor 305	. . . . . . 7 |- (-. (v e. U.(x \ {z}) /\ v e. z) <-> (-. v e. U.(x \ {z}) \/ -. v e. z))
8		eluni 2496	. . . . . . . . . 10 |- (v e. U.(x \ {z}) <-> E.w(v e. w /\ w e. (x \ {z})))
9	8	anbi1i 480	. . . . . . . . 9 |- ((v e. U.(x \ {z}) /\ v e. z) <-> (E.w(v e. w /\ w e. (x \ {z})) /\ v e. z))
10		df-rex 1642	. . . . . . . . . 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		eldifsn 2453	. . . . . . . . . . . . . . 15 |- (w e. (x \ {z}) <-> (w e. x /\ w =/= z))
12		necom 1628	. . . . . . . . . . . . . . . 16 |- (w =/= z <-> z =/= w)
13	12	anbi2i 479	. . . . . . . . . . . . . . 15 |- ((w e. x /\ w =/= z) <-> (w e. x /\ z =/= w))
14	11, 13	bitr 173	. . . . . . . . . . . . . 14 |- (w e. (x \ {z}) <-> (w e. x /\ z =/= w))
15	14	anbi2i 479	. . . . . . . . . . . . 13 |- (((v e. w /\ v e. z) /\ w e. (x \ {z})) <-> ((v e. w /\ v e. z) /\ (w e. x /\ z =/= w)))
16		ancom 435	. . . . . . . . . . . . . . 15 |- ((v e. w /\ v e. z) <-> (v e. z /\ v e. w))
17	16	anbi1i 480	. . . . . . . . . . . . . 14 |- (((v e. w /\ v e. z) /\ (w e. x /\ z =/= w)) <-> ((v e. z /\ v e. w) /\ (w e. x /\ z =/= w)))
18		ancom 435	. . . . . . . . . . . . . 14 |- (((v e. z /\ v e. w) /\ (w e. x /\ z =/= w)) <-> ((w e. x /\ z =/= w) /\ (v e. z /\ v e. w)))
19	17, 18	bitr 173	. . . . . . . . . . . . 13 |- (((v e. w /\ v e. z) /\ (w e. x /\ z =/= w)) <-> ((w e. x /\ z =/= w) /\ (v e. z /\ v e. w)))
20		anass 439	. . . . . . . . . . . . 13 |- (((w e. x /\ z =/= w) /\ (v e. z /\ v e. w)) <-> (w e. x /\ (z =/= w /\ (v e. z /\ v e. w))))
21	15, 19, 20	3bitr 177	. . . . . . . . . . . 12 |- (((v e. w /\ v e. z) /\ w e. (x \ {z})) <-> (w e. x /\ (z =/= w /\ (v e. z /\ v e. w))))
22		an23 484	. . . . . . . . . . . 12 |- (((v e. w /\ v e. z) /\ w e. (x \ {z})) <-> ((v e. w /\ w e. (x \ {z})) /\ v e. z))
23		elin 2197	. . . . . . . . . . . . . . 15 |- (v e. (z i^i w) <-> (v e. z /\ v e. w))
24	23	anbi2i 479	. . . . . . . . . . . . . 14 |- ((z =/= w /\ v e. (z i^i w)) <-> (z =/= w /\ (v e. z /\ v e. w)))
25		df-an 225	. . . . . . . . . . . . . 14 |- ((z =/= w /\ v e. (z i^i w)) <-> -. (z =/= w -> -. v e. (z i^i w)))
26	24, 25	bitr3 175	. . . . . . . . . . . . 13 |- ((z =/= w /\ (v e. z /\ v e. w)) <-> -. (z =/= w -> -. v e. (z i^i w)))
27	26	anbi2i 479	. . . . . . . . . . . 12 |- ((w e. x /\ (z =/= w /\ (v e. z /\ v e. w))) <-> (w e. x /\ -. (z =/= w -> -. v e. (z i^i w))))
28	21, 22, 27	3bitr3r 182	. . . . . . . . . . 11 |- ((w e. x /\ -. (z =/= w -> -. v e. (z i^i w))) <-> ((v e. w /\ w e. (x \ {z})) /\ v e. z))
29	28	exbii 1047	. . . . . . . . . 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))
30		19.41v 1300	. . . . . . . . . 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))
31	10, 29, 30	3bitr 177	. . . . . . . . 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))
32		rexnal 1646	. . . . . . . . 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)))
33	9, 31, 32	3bitr2r 180	. . . . . . . 8 |- (-. A.w e. x (z =/= w -> -. v e. (z i^i w)) <-> (v e. U.(x \ {z}) /\ v e. z))
34	33	con1bii 220	. . . . . . 7 |- (-. (v e. U.(x \ {z}) /\ v e. z) <-> A.w e. x (z =/= w -> -. v e. (z i^i w)))
35	7, 34	bitr3 175	. . . . . 6 |- ((-. v e. U.(x \ {z}) \/ -. v e. z) <-> A.w e. x (z =/= w -> -. v e. (z i^i w)))
36	35	a1i 8	. . . . 5 |- (v e. z -> ((-. v e. U.(x \ {z}) \/ -. v e. z) <-> A.w e. x (z =/= w -> -. v e. (z i^i w))))
37	36	rabbii 1796	. . . 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))}
38	1, 6, 37	3eqtr 1491	. . 3 |- (z \ U.(x \ {z})) = {v e. z | A.w e. x (z =/= w -> -. v e. (z i^i w))}
39	38	neeq1i 1584	. 2 |- ((z \ U.(x \ {z})) =/= (/) <-> {v e. z | A.w e. x (z =/= w -> -. v e. (z i^i w))} =/= (/))
40		rabn0 2282	. 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)))
41	39, 40	bitr 173	1 |- ((z \ U.(x \ {z})) =/= (/) <-> E.v e. z A.w e. x (z =/= w -> -. v e. (z i^i w)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   e. wcel 955  E.wex 977   =/= wne 1577  A.wral 1637  E.wrex 1638  {crab 1640   \ cdif 2034   u. cun 2035   i^i cin 2036  (/)c0 2270  {csn 2399  U.cuni 2493

This theorem is referenced by:  kmlem13 4749

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-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-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-rab 1644  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-nul 2271  df-sn 2402  df-pr 2403  df-uni 2494

Copyright terms: Public domain