Theorem kmlem2 8552

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.)

Assertion

Ref	Expression
kmlem2

Distinct variable groups:   ,,   ,,,

Proof of Theorem kmlem2

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

Step	Hyp	Ref	Expression
1		ineq2 3693	. . . . . . . 8
2	1	eleq2d 2527	. . . . . . 7
3	2	eubidv 2304	. . . . . 6
4	3	imbi2d 316	. . . . 5
5	4	ralbidv 2896	. . . 4
6	5	cbvexv 2024	. . 3
7		vex 3112	. . . . . . 7
8	7	uniex 6596	. . . . . 6
9		eleq2 2530	. . . . . . . 8
10	9	notbid 294	. . . . . . 7
11	10	exbidv 1714	. . . . . 6
12		nalset 4589	. . . . . . . 8
13		alexn 1664	. . . . . . . 8
14	12, 13	mpbir 209	. . . . . . 7
15	14	spi 1864	. . . . . 6
16	8, 11, 15	vtocl 3161	. . . . 5
17		indi 3743	. . . . . . . . . . . . 13
18		elssuni 4279	. . . . . . . . . . . . . . . . . 18
19	18	ssneld 3505	. . . . . . . . . . . . . . . . 17
20		disjsn 4090	. . . . . . . . . . . . . . . . 17
21	19, 20	syl6ibr 227	. . . . . . . . . . . . . . . 16
22	21	impcom 430	. . . . . . . . . . . . . . 15
23	22	uneq2d 3657	. . . . . . . . . . . . . 14
24		un0 3810	. . . . . . . . . . . . . 14
25	23, 24	syl6eq 2514	. . . . . . . . . . . . 13
26	17, 25	syl5req 2511	. . . . . . . . . . . 12
27	26	eleq2d 2527	. . . . . . . . . . 11
28	27	eubidv 2304	. . . . . . . . . 10
29	28	imbi2d 316	. . . . . . . . 9
30	29	ralbidva 2893	. . . . . . . 8
31		ssnid 4058	. . . . . . . . . . . . 13
32	31	olci 391	. . . . . . . . . . . 12
33		elun 3644	. . . . . . . . . . . 12
34	32, 33	mpbir 209	. . . . . . . . . . 11
35		elssuni 4279	. . . . . . . . . . . 12
36	35	sseld 3502	. . . . . . . . . . 11
37	34, 36	mpi 17	. . . . . . . . . 10
38	37	con3i 135	. . . . . . . . 9
39	38	biantrurd 508	. . . . . . . 8
40	30, 39	bitrd 253	. . . . . . 7
41		vex 3112	. . . . . . . . 9
42		snex 4693	. . . . . . . . 9
43	41, 42	unex 6598	. . . . . . . 8
44		eleq1 2529	. . . . . . . . . 10
45	44	notbid 294	. . . . . . . . 9
46		ineq2 3693	. . . . . . . . . . . . 13
47	46	eleq2d 2527	. . . . . . . . . . . 12
48	47	eubidv 2304	. . . . . . . . . . 11
49	48	imbi2d 316	. . . . . . . . . 10
50	49	ralbidv 2896	. . . . . . . . 9
51	45, 50	anbi12d 710	. . . . . . . 8
52	43, 51	spcev 3201	. . . . . . 7
53	40, 52	syl6bi 228	. . . . . 6
54	53	exlimiv 1722	. . . . 5
55	16, 54	ax-mp 5	. . . 4
56	55	exlimiv 1722	. . 3
57	6, 56	sylbi 195	. 2
58		exsimpr 1678	. 2
59	57, 58	impbii 188	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  E!weu 2282  A.wral 2807  u.cun 3473  i^icin 3474  c0 3784  {csn 4029  U.cuni 4249

This theorem is referenced by:  kmlem8  8558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691  ax-un 6592

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-sn 4030  df-pr 4032  df-uni 4250