Theorem mayetes3i 28588

Description: Mayet's equation E^*₃, derived from E₃. Solution, for n = 3, to open problem in Remark (b) after Theorem 7.1 of [Mayet3] p. 1240. (Contributed by NM, 10-May-2009.) (New usage is discouraged.)

Hypotheses

Ref	Expression
mayetes3.a	|- A e. CH
mayetes3.b	|- B e. CH
mayetes3.c	|- C e. CH
mayetes3.d	|- D e. CH
mayetes3.f	|- F e. CH
mayetes3.g	|- G e. CH
mayetes3.r	|- R e. CH
mayetes3.ac	|- A C_ ( _|_ ` C )
mayetes3.af	|- A C_ ( _|_ ` F )
mayetes3.cf	|- C C_ ( _|_ ` F )
mayetes3.ab	|- A C_ ( _|_ ` B )
mayetes3.cd	|- C C_ ( _|_ ` D )
mayetes3.fg	|- F C_ ( _|_ ` G )
mayetes3.rx	|- R C_ ( _|_ ` X )
mayetes3.x	|- X = ( ( A vH C ) vH F )
mayetes3.y	|- Y = ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) )
mayetes3.z	|- Z = ( ( B vH D ) vH G )

Assertion

Ref	Expression
mayetes3i	|- ( ( X vH R ) i^i Y ) C_ ( Z vH R )

Proof of Theorem mayetes3i

Step	Hyp	Ref	Expression
1		mayetes3.a	. . . . . . . . 9 |- A e. CH
2		mayetes3.c	. . . . . . . . 9 |- C e. CH
3	1, 2	chjcli 28316	. . . . . . . 8 |- ( A vH C ) e. CH
4		mayetes3.f	. . . . . . . 8 |- F e. CH
5	3, 4	chjcli 28316	. . . . . . 7 |- ( ( A vH C ) vH F ) e. CH
6		mayetes3.r	. . . . . . 7 |- R e. CH
7	5, 6	chjcomi 28327	. . . . . 6 |- ( ( ( A vH C ) vH F ) vH R ) = ( R vH ( ( A vH C ) vH F ) )
8	7	eqimssi 3659	. . . . 5 |- ( ( ( A vH C ) vH F ) vH R ) C_ ( R vH ( ( A vH C ) vH F ) )
9		mayetes3.b	. . . . . . . . . . 11 |- B e. CH
10	1, 9	chjcli 28316	. . . . . . . . . 10 |- ( A vH B ) e. CH
11	10, 6	chub1i 28328	. . . . . . . . 9 |- ( A vH B ) C_ ( ( A vH B ) vH R )
12	1, 9, 6	chjassi 28345	. . . . . . . . 9 |- ( ( A vH B ) vH R ) = ( A vH ( B vH R ) )
13	11, 12	sseqtri 3637	. . . . . . . 8 |- ( A vH B ) C_ ( A vH ( B vH R ) )
14	9, 6	chjcli 28316	. . . . . . . . . 10 |- ( B vH R ) e. CH
15	1, 14	chjcli 28316	. . . . . . . . 9 |- ( A vH ( B vH R ) ) e. CH
16	15, 6	chub2i 28329	. . . . . . . 8 |- ( A vH ( B vH R ) ) C_ ( R vH ( A vH ( B vH R ) ) )
17	13, 16	sstri 3612	. . . . . . 7 |- ( A vH B ) C_ ( R vH ( A vH ( B vH R ) ) )
18		mayetes3.d	. . . . . . . . . . 11 |- D e. CH
19	2, 18	chjcli 28316	. . . . . . . . . 10 |- ( C vH D ) e. CH
20	19, 6	chub1i 28328	. . . . . . . . 9 |- ( C vH D ) C_ ( ( C vH D ) vH R )
21	2, 18, 6	chjassi 28345	. . . . . . . . 9 |- ( ( C vH D ) vH R ) = ( C vH ( D vH R ) )
22	20, 21	sseqtri 3637	. . . . . . . 8 |- ( C vH D ) C_ ( C vH ( D vH R ) )
23	18, 6	chjcli 28316	. . . . . . . . . 10 |- ( D vH R ) e. CH
24	2, 23	chjcli 28316	. . . . . . . . 9 |- ( C vH ( D vH R ) ) e. CH
25	24, 6	chub2i 28329	. . . . . . . 8 |- ( C vH ( D vH R ) ) C_ ( R vH ( C vH ( D vH R ) ) )
26	22, 25	sstri 3612	. . . . . . 7 |- ( C vH D ) C_ ( R vH ( C vH ( D vH R ) ) )
27		ss2in 3840	. . . . . . 7 |- ( ( ( A vH B ) C_ ( R vH ( A vH ( B vH R ) ) ) /\ ( C vH D ) C_ ( R vH ( C vH ( D vH R ) ) ) ) -> ( ( A vH B ) i^i ( C vH D ) ) C_ ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) )
28	17, 26, 27	mp2an 708	. . . . . 6 |- ( ( A vH B ) i^i ( C vH D ) ) C_ ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) )
29		mayetes3.g	. . . . . . . . . 10 |- G e. CH
30	4, 29	chjcli 28316	. . . . . . . . 9 |- ( F vH G ) e. CH
31	30, 6	chub1i 28328	. . . . . . . 8 |- ( F vH G ) C_ ( ( F vH G ) vH R )
32	4, 29, 6	chjassi 28345	. . . . . . . 8 |- ( ( F vH G ) vH R ) = ( F vH ( G vH R ) )
33	31, 32	sseqtri 3637	. . . . . . 7 |- ( F vH G ) C_ ( F vH ( G vH R ) )
34	29, 6	chjcli 28316	. . . . . . . . 9 |- ( G vH R ) e. CH
35	4, 34	chjcli 28316	. . . . . . . 8 |- ( F vH ( G vH R ) ) e. CH
36	35, 6	chub2i 28329	. . . . . . 7 |- ( F vH ( G vH R ) ) C_ ( R vH ( F vH ( G vH R ) ) )
37	33, 36	sstri 3612	. . . . . 6 |- ( F vH G ) C_ ( R vH ( F vH ( G vH R ) ) )
38		ss2in 3840	. . . . . 6 |- ( ( ( ( A vH B ) i^i ( C vH D ) ) C_ ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) /\ ( F vH G ) C_ ( R vH ( F vH ( G vH R ) ) ) ) -> ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) C_ ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) )
39	28, 37, 38	mp2an 708	. . . . 5 |- ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) C_ ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) )
40		ss2in 3840	. . . . 5 |- ( ( ( ( ( A vH C ) vH F ) vH R ) C_ ( R vH ( ( A vH C ) vH F ) ) /\ ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) C_ ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) ) -> ( ( ( ( A vH C ) vH F ) vH R ) i^i ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) ) C_ ( ( R vH ( ( A vH C ) vH F ) ) i^i ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) ) )
41	8, 39, 40	mp2an 708	. . . 4 |- ( ( ( ( A vH C ) vH F ) vH R ) i^i ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) ) C_ ( ( R vH ( ( A vH C ) vH F ) ) i^i ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) )
42	15, 24	chincli 28319	. . . . . . 7 |- ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) e. CH
43	42, 35	chincli 28319	. . . . . 6 |- ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) e. CH
44		mayetes3.x	. . . . . . . . . . 11 |- X = ( ( A vH C ) vH F )
45	44, 5	eqeltri 2697	. . . . . . . . . 10 |- X e. CH
46	45	choccli 28166	. . . . . . . . 9 |- ( _|_ ` X ) e. CH
47		mayetes3.rx	. . . . . . . . 9 |- R C_ ( _|_ ` X )
48	6, 46, 47	lecmii 28462	. . . . . . . 8 |- R C_H ( _|_ ` X )
49	6, 45	cmcm2i 28452	. . . . . . . 8 |- ( R C_H X <-> R C_H ( _|_ ` X ) )
50	48, 49	mpbir 221	. . . . . . 7 |- R C_H X
51	50, 44	breqtri 4678	. . . . . 6 |- R C_H ( ( A vH C ) vH F )
52	6, 9	chub2i 28329	. . . . . . . . . 10 |- R C_ ( B vH R )
53	14, 1	chub2i 28329	. . . . . . . . . 10 |- ( B vH R ) C_ ( A vH ( B vH R ) )
54	52, 53	sstri 3612	. . . . . . . . 9 |- R C_ ( A vH ( B vH R ) )
55	6, 15, 54	lecmii 28462	. . . . . . . 8 |- R C_H ( A vH ( B vH R ) )
56	6, 18	chub2i 28329	. . . . . . . . . 10 |- R C_ ( D vH R )
57	23, 2	chub2i 28329	. . . . . . . . . 10 |- ( D vH R ) C_ ( C vH ( D vH R ) )
58	56, 57	sstri 3612	. . . . . . . . 9 |- R C_ ( C vH ( D vH R ) )
59	6, 24, 58	lecmii 28462	. . . . . . . 8 |- R C_H ( C vH ( D vH R ) )
60	6, 15, 24, 55, 59	cm2mi 28485	. . . . . . 7 |- R C_H ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) )
61	6, 29	chub2i 28329	. . . . . . . . 9 |- R C_ ( G vH R )
62	34, 4	chub2i 28329	. . . . . . . . 9 |- ( G vH R ) C_ ( F vH ( G vH R ) )
63	61, 62	sstri 3612	. . . . . . . 8 |- R C_ ( F vH ( G vH R ) )
64	6, 35, 63	lecmii 28462	. . . . . . 7 |- R C_H ( F vH ( G vH R ) )
65	6, 42, 35, 60, 64	cm2mi 28485	. . . . . 6 |- R C_H ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) )
66	6, 5, 43, 51, 65	fh3i 28482	. . . . 5 |- ( R vH ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) ) = ( ( R vH ( ( A vH C ) vH F ) ) i^i ( R vH ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) )
67	6, 42, 35, 60, 64	fh3i 28482	. . . . . . 7 |- ( R vH ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) = ( ( R vH ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) )
68	6, 15, 24, 55, 59	fh3i 28482	. . . . . . . 8 |- ( R vH ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) ) = ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) )
69	68	ineq1i 3810	. . . . . . 7 |- ( ( R vH ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) = ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) )
70	67, 69	eqtri 2644	. . . . . 6 |- ( R vH ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) = ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) )
71	70	ineq2i 3811	. . . . 5 |- ( ( R vH ( ( A vH C ) vH F ) ) i^i ( R vH ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) ) = ( ( R vH ( ( A vH C ) vH F ) ) i^i ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) )
72	66, 71	eqtr2i 2645	. . . 4 |- ( ( R vH ( ( A vH C ) vH F ) ) i^i ( ( ( R vH ( A vH ( B vH R ) ) ) i^i ( R vH ( C vH ( D vH R ) ) ) ) i^i ( R vH ( F vH ( G vH R ) ) ) ) ) = ( R vH ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) )
73	41, 72	sseqtri 3637	. . 3 |- ( ( ( ( A vH C ) vH F ) vH R ) i^i ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) ) C_ ( R vH ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) )
74	9, 18	chjcli 28316	. . . . . 6 |- ( B vH D ) e. CH
75	74, 29	chjcli 28316	. . . . 5 |- ( ( B vH D ) vH G ) e. CH
76	6, 75	chub2i 28329	. . . 4 |- R C_ ( ( ( B vH D ) vH G ) vH R )
77		mayetes3.ac	. . . . 5 |- A C_ ( _|_ ` C )
78		mayetes3.af	. . . . 5 |- A C_ ( _|_ ` F )
79		mayetes3.cf	. . . . 5 |- C C_ ( _|_ ` F )
80		mayetes3.ab	. . . . . . 7 |- A C_ ( _|_ ` B )
81	1, 2	chub1i 28328	. . . . . . . . . . 11 |- A C_ ( A vH C )
82	3, 4	chub1i 28328	. . . . . . . . . . . 12 |- ( A vH C ) C_ ( ( A vH C ) vH F )
83	82, 44	sseqtr4i 3638	. . . . . . . . . . 11 |- ( A vH C ) C_ X
84	81, 83	sstri 3612	. . . . . . . . . 10 |- A C_ X
85	1, 45	chsscon3i 28320	. . . . . . . . . 10 |- ( A C_ X <-> ( _|_ ` X ) C_ ( _|_ ` A ) )
86	84, 85	mpbi 220	. . . . . . . . 9 |- ( _|_ ` X ) C_ ( _|_ ` A )
87	47, 86	sstri 3612	. . . . . . . 8 |- R C_ ( _|_ ` A )
88	6, 1	chsscon2i 28322	. . . . . . . 8 |- ( R C_ ( _|_ ` A ) <-> A C_ ( _|_ ` R ) )
89	87, 88	mpbi 220	. . . . . . 7 |- A C_ ( _|_ ` R )
90	80, 89	ssini 3836	. . . . . 6 |- A C_ ( ( _|_ ` B ) i^i ( _|_ ` R ) )
91	9, 6	chdmj1i 28340	. . . . . 6 |- ( _|_ ` ( B vH R ) ) = ( ( _|_ ` B ) i^i ( _|_ ` R ) )
92	90, 91	sseqtr4i 3638	. . . . 5 |- A C_ ( _|_ ` ( B vH R ) )
93		mayetes3.cd	. . . . . . 7 |- C C_ ( _|_ ` D )
94	2, 1	chub2i 28329	. . . . . . . . . . 11 |- C C_ ( A vH C )
95	94, 83	sstri 3612	. . . . . . . . . 10 |- C C_ X
96	2, 45	chsscon3i 28320	. . . . . . . . . 10 |- ( C C_ X <-> ( _|_ ` X ) C_ ( _|_ ` C ) )
97	95, 96	mpbi 220	. . . . . . . . 9 |- ( _|_ ` X ) C_ ( _|_ ` C )
98	47, 97	sstri 3612	. . . . . . . 8 |- R C_ ( _|_ ` C )
99	6, 2	chsscon2i 28322	. . . . . . . 8 |- ( R C_ ( _|_ ` C ) <-> C C_ ( _|_ ` R ) )
100	98, 99	mpbi 220	. . . . . . 7 |- C C_ ( _|_ ` R )
101	93, 100	ssini 3836	. . . . . 6 |- C C_ ( ( _|_ ` D ) i^i ( _|_ ` R ) )
102	18, 6	chdmj1i 28340	. . . . . 6 |- ( _|_ ` ( D vH R ) ) = ( ( _|_ ` D ) i^i ( _|_ ` R ) )
103	101, 102	sseqtr4i 3638	. . . . 5 |- C C_ ( _|_ ` ( D vH R ) )
104		mayetes3.fg	. . . . . . 7 |- F C_ ( _|_ ` G )
105	4, 3	chub2i 28329	. . . . . . . . . . 11 |- F C_ ( ( A vH C ) vH F )
106	105, 44	sseqtr4i 3638	. . . . . . . . . 10 |- F C_ X
107	4, 45	chsscon3i 28320	. . . . . . . . . 10 |- ( F C_ X <-> ( _|_ ` X ) C_ ( _|_ ` F ) )
108	106, 107	mpbi 220	. . . . . . . . 9 |- ( _|_ ` X ) C_ ( _|_ ` F )
109	47, 108	sstri 3612	. . . . . . . 8 |- R C_ ( _|_ ` F )
110	6, 4	chsscon2i 28322	. . . . . . . 8 |- ( R C_ ( _|_ ` F ) <-> F C_ ( _|_ ` R ) )
111	109, 110	mpbi 220	. . . . . . 7 |- F C_ ( _|_ ` R )
112	104, 111	ssini 3836	. . . . . 6 |- F C_ ( ( _|_ ` G ) i^i ( _|_ ` R ) )
113	29, 6	chdmj1i 28340	. . . . . 6 |- ( _|_ ` ( G vH R ) ) = ( ( _|_ ` G ) i^i ( _|_ ` R ) )
114	112, 113	sseqtr4i 3638	. . . . 5 |- F C_ ( _|_ ` ( G vH R ) )
115		eqid 2622	. . . . 5 |- ( ( A vH C ) vH F ) = ( ( A vH C ) vH F )
116		eqid 2622	. . . . 5 |- ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) = ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) )
117	74, 29, 6	chjjdiri 28383	. . . . . 6 |- ( ( ( B vH D ) vH G ) vH R ) = ( ( ( B vH D ) vH R ) vH ( G vH R ) )
118	9, 18, 6	chjjdiri 28383	. . . . . . 7 |- ( ( B vH D ) vH R ) = ( ( B vH R ) vH ( D vH R ) )
119	118	oveq1i 6660	. . . . . 6 |- ( ( ( B vH D ) vH R ) vH ( G vH R ) ) = ( ( ( B vH R ) vH ( D vH R ) ) vH ( G vH R ) )
120	117, 119	eqtri 2644	. . . . 5 |- ( ( ( B vH D ) vH G ) vH R ) = ( ( ( B vH R ) vH ( D vH R ) ) vH ( G vH R ) )
121	1, 14, 2, 23, 4, 34, 77, 78, 79, 92, 103, 114, 115, 116, 120	mayete3i 28587	. . . 4 |- ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) C_ ( ( ( B vH D ) vH G ) vH R )
122	5, 43	chincli 28319	. . . . 5 |- ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) e. CH
123	75, 6	chjcli 28316	. . . . 5 |- ( ( ( B vH D ) vH G ) vH R ) e. CH
124	6, 122, 123	chlubii 28331	. . . 4 |- ( ( R C_ ( ( ( B vH D ) vH G ) vH R ) /\ ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) C_ ( ( ( B vH D ) vH G ) vH R ) ) -> ( R vH ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) ) C_ ( ( ( B vH D ) vH G ) vH R ) )
125	76, 121, 124	mp2an 708	. . 3 |- ( R vH ( ( ( A vH C ) vH F ) i^i ( ( ( A vH ( B vH R ) ) i^i ( C vH ( D vH R ) ) ) i^i ( F vH ( G vH R ) ) ) ) ) C_ ( ( ( B vH D ) vH G ) vH R )
126	73, 125	sstri 3612	. 2 |- ( ( ( ( A vH C ) vH F ) vH R ) i^i ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) ) C_ ( ( ( B vH D ) vH G ) vH R )
127	44	oveq1i 6660	. . 3 |- ( X vH R ) = ( ( ( A vH C ) vH F ) vH R )
128		mayetes3.y	. . 3 |- Y = ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) )
129	127, 128	ineq12i 3812	. 2 |- ( ( X vH R ) i^i Y ) = ( ( ( ( A vH C ) vH F ) vH R ) i^i ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( F vH G ) ) )
130		mayetes3.z	. . 3 |- Z = ( ( B vH D ) vH G )
131	130	oveq1i 6660	. 2 |- ( Z vH R ) = ( ( ( B vH D ) vH G ) vH R )
132	126, 129, 131	3sstr4i 3644	1 |- ( ( X vH R ) i^i Y ) C_ ( Z vH R )

Syntax hints:   = wceq 1483   e. wcel 1990   i^i cin 3573   C_ wss 3574   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   CHcch 27786   _|_cort 27787   vH chj 27790   C_H ccm 27793

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-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cc 9257  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016  ax-hilex 27856  ax-hfvadd 27857  ax-hvcom 27858  ax-hvass 27859  ax-hv0cl 27860  ax-hvaddid 27861  ax-hfvmul 27862  ax-hvmulid 27863  ax-hvmulass 27864  ax-hvdistr1 27865  ax-hvdistr2 27866  ax-hvmul0 27867  ax-hfi 27936  ax-his1 27939  ax-his2 27940  ax-his3 27941  ax-his4 27942  ax-hcompl 28059

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-sum 14417  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-cn 21031  df-cnp 21032  df-lm 21033  df-haus 21119  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cfil 23053  df-cau 23054  df-cmet 23055  df-grpo 27347  df-gid 27348  df-ginv 27349  df-gdiv 27350  df-ablo 27399  df-vc 27414  df-nv 27447  df-va 27450  df-ba 27451  df-sm 27452  df-0v 27453  df-vs 27454  df-nmcv 27455  df-ims 27456  df-dip 27556  df-ssp 27577  df-ph 27668  df-cbn 27719  df-hnorm 27825  df-hba 27826  df-hvsub 27828  df-hlim 27829  df-hcau 27830  df-sh 28064  df-ch 28078  df-oc 28109  df-ch0 28110  df-shs 28167  df-chj 28169  df-pjh 28254  df-cm 28442

This theorem is referenced by: (None)