athgt - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > athgt		Structured version Unicode version

Theorem athgt 32940

Description: A Hilbert lattice, whose height is at least 4, has a chain of 4 successively covering atom joins. (Contributed by NM, 3-May-2012.)

**Hypotheses**
Ref	Expression
athgt.j	$.\/$
athgt.c
athgt.a

**Assertion**
Ref	Expression
athgt	$.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$

Distinct variable groups:

$.\/$ ,

Allowed substitution hints:

(

) $.\/$ (

)

Proof of Theorem athgt Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2438	. . 3
2		eqid 2438	. . 3
3		eqid 2438	. . 3
4		eqid 2438	. . 3
5	1, 2, 3, 4	hlhgt4 32872	. 2 $/\$ $/\$ $/\$
6		simpl1 991	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		hlop 32847	. . . . . . . . . 10
8	1, 3	op0cl 32669	. . . . . . . . . 10
9	6, 7, 8	3syl 20	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simpl2l 1041	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simprll 761	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		eqid 2438	. . . . . . . . . 10
13		athgt.j	. . . . . . . . . 10 $.\/$
14		athgt.c	. . . . . . . . . 10
15		athgt.a	. . . . . . . . . 10
16	1, 12, 2, 13, 14, 15	hlrelat3 32896	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
17	6, 9, 10, 11, 16	syl31anc 1221	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
18		simp11 1018	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simp3 990	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20	3, 14, 15	atcvr0 32773	. . . . . . . . . . . . . 14 $/\$
21	18, 19, 20	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		hlol 32846	. . . . . . . . . . . . . . 15
23	18, 22	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24	1, 15	atbase 32774	. . . . . . . . . . . . . . 15
25	24	3ad2ant3 1011	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	1, 13, 3	olj02 32711	. . . . . . . . . . . . . 14 $/\$ $.\/$
27	23, 25, 26	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
28	21, 27	breqtrrd 4313	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29	28	biantrurd 508	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
30	27	breq1d 4297	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
31	29, 30	bitr3d 255	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
32	31	3expa 1187	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
33	32	rexbidva 2727	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
34	17, 33	mpbid 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		simp11 1018	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36	25	3adant3r 1215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		simp12r 1102	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simp3r 1017	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		simp2lr 1056	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		hlpos 32850	. . . . . . . . . . . . . . 15
41	35, 40	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simp12l 1101	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	1, 12, 2	plelttr 15134	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
44	41, 36, 42, 37, 43	syl13anc 1220	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	38, 39, 44	mp2and 679	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	1, 12, 2, 13, 14, 15	hlrelat3 32896	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
47	35, 36, 37, 45, 46	syl31anc 1221	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
48		simp11 1018	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49		hllat 32848	. . . . . . . . . . . . . . . . . . . . . . . 24
50	48, 49	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
51		simp3ll 1059	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
52	51, 24	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
53		simp3lr 1060	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
54	1, 15	atbase 32774	. . . . . . . . . . . . . . . . . . . . . . . 24
55	53, 54	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
56	1, 13	latjcl 15213	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $.\/$
57	50, 52, 55, 56	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
58		simp13 1020	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
59		simp3r 1017	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
60		simp2l 1014	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
61	48, 40	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
62		simp12 1019	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
63	1, 12, 2	plelttr 15134	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
64	61, 57, 62, 58, 63	syl13anc 1220	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
65	59, 60, 64	mp2and 679	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
66	1, 12, 2, 13, 14, 15	hlrelat3 32896	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
67	48, 57, 58, 65, 66	syl31anc 1221	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
68		simp1ll 1051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
69	68, 49	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
70		simp2ll 1055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
71	70, 24	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
72		simp2lr 1056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
73	72, 54	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
74	69, 71, 73, 56	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
75		simp3l 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
76	1, 15	atbase 32774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77	75, 76	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
78	1, 13	latjcl 15213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $.\/$ $/\$ $.\/$ $.\/$
79	69, 74, 77, 78	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
80	1, 4	op1cl 32670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
81	68, 7, 80	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
82		simp3r 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
83		simp1r 1013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
84	68, 40	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
85		simp1lr 1052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
86	1, 12, 2	plelttr 15134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
87	84, 79, 85, 81, 86	syl13anc 1220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
88	82, 83, 87	mp2and 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
89	1, 12, 2, 13, 14, 15	hlrelat3 32896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
90	68, 79, 81, 88, 89	syl31anc 1221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
91		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
92	91	reximi 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
93	90, 92	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
94	93	3exp 1186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
95	94	exp4a 606	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
96	95	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
97	96	3adant2 1007	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
98	97	3imp 1181	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
99	98	3adant2l 1212	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
100	99	imp 429	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
101	100	anim2d 565	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
102	101	reximdva 2823	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
103	67, 102	mpd 15	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
104	103	3exp 1186	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
105	104	exp4a 606	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
106	105	exp4a 606	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
107	106	3adant2l 1212	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
108	107	3imp1 1200	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
109	108	anim2d 565	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
110	109	reximdva 2823	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
111	110	3adant2l 1212	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
112	111	3adant3r 1215	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
113	47, 112	mpd 15	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
114	113	3expia 1189	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
115	114	expd 436	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
116	115	reximdvai 2821	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
117	34, 116	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
118	117	3exp1 1203	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
119	118	imp 429	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
120	119	rexlimdv 2835	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
121	120	rexlimdvva 2843	. 2 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
122	5, 121	mpd 15	1 $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

wrex 2711 class class class wbr 4287

cfv 5413 (class class class)co 6086

cbs 14166

cple 14237

cpo 15102

cplt 15103

cjn 15106

cp0 15199

cp1 15200

clat 15207

cops 32657

col 32659

ccvr 32747

catm 32748

chlt 32835

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-ral 2715 df-rex 2716 df-reu 2717 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-op 3879 df-uni 4087 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-id 4631 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-oprab 6090 df-poset 15108 df-plt 15120 df-lub 15136 df-glb 15137 df-join 15138 df-meet 15139 df-p0 15201 df-p1 15202 df-lat 15208 df-clat 15270 df-oposet 32661 df-ol 32663 df-oml 32664 df-covers 32751 df-ats 32752 df-atl 32783 df-cvlat 32807 df-hlat 32836

This theorem is referenced by: 3dim0 32941

W3C validator