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 33439

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 2454	. . 3
2		eqid 2454	. . 3
3		eqid 2454	. . 3
4		eqid 2454	. . 3
5	1, 2, 3, 4	hlhgt4 33371	. 2 $/\$ $/\$ $/\$
6		simpl1 991	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		hlop 33346	. . . . . . . . . 10
8	1, 3	op0cl 33168	. . . . . . . . . 10
9	6, 7, 8	3syl 20	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simpl2l 1041	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simprll 761	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		eqid 2454	. . . . . . . . . 10
13		athgt.j	. . . . . . . . . 10 $.\/$
14		athgt.c	. . . . . . . . . 10
15		athgt.a	. . . . . . . . . 10
16	1, 12, 2, 13, 14, 15	hlrelat3 33395	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
17	6, 9, 10, 11, 16	syl31anc 1222	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
18		simp11 1018	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simp3 990	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20	3, 14, 15	atcvr0 33272	. . . . . . . . . . . . . 14 $/\$
21	18, 19, 20	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		hlol 33345	. . . . . . . . . . . . . . 15
23	18, 22	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24	1, 15	atbase 33273	. . . . . . . . . . . . . . 15
25	24	3ad2ant3 1011	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	1, 13, 3	olj02 33210	. . . . . . . . . . . . . 14 $/\$ $.\/$
27	23, 25, 26	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
28	21, 27	breqtrrd 4427	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29	28	biantrurd 508	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
30	27	breq1d 4411	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
31	29, 30	bitr3d 255	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
32	31	3expa 1188	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
33	32	rexbidva 2865	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
34	17, 33	mpbid 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		simp11 1018	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36	25	3adant3r 1216	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		simp12r 1102	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simp3r 1017	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		simp2lr 1056	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		hlpos 33349	. . . . . . . . . . . . . . 15
41	35, 40	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simp12l 1101	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	1, 12, 2	plelttr 15262	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
44	41, 36, 42, 37, 43	syl13anc 1221	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	38, 39, 44	mp2and 679	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	1, 12, 2, 13, 14, 15	hlrelat3 33395	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
47	35, 36, 37, 45, 46	syl31anc 1222	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
48		simp11 1018	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49		hllat 33347	. . . . . . . . . . . . . . . . . . . . . . . 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 33273	. . . . . . . . . . . . . . . . . . . . . . . 24
55	53, 54	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
56	1, 13	latjcl 15341	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $.\/$
57	50, 52, 55, 56	syl3anc 1219	. . . . . . . . . . . . . . . . . . . . . 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 15262	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
64	61, 57, 62, 58, 63	syl13anc 1221	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
65	59, 60, 64	mp2and 679	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
66	1, 12, 2, 13, 14, 15	hlrelat3 33395	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
67	48, 57, 58, 65, 66	syl31anc 1222	. . . . . . . . . . . . . . . . . . . . 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 1219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
75		simp3l 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
76	1, 15	atbase 33273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77	75, 76	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
78	1, 13	latjcl 15341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $.\/$ $/\$ $.\/$ $.\/$
79	69, 74, 77, 78	syl3anc 1219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
80	1, 4	op1cl 33169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 15262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
87	84, 79, 85, 81, 86	syl13anc 1221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
88	82, 83, 87	mp2and 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
89	1, 12, 2, 13, 14, 15	hlrelat3 33395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
90	68, 79, 81, 88, 89	syl31anc 1222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
91		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
92	91	reximi 2929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
93	90, 92	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
94	93	3exp 1187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
95	94	exp4a 606	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
96	95	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
97	96	3adant2 1007	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
98	97	3imp 1182	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
99	98	3adant2l 1213	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
100	99	imp 429	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
101	100	anim2d 565	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
102	101	reximdva 2934	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
103	67, 102	mpd 15	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
104	103	3exp 1187	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
105	104	exp4a 606	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
106	105	exp4a 606	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
107	106	3adant2l 1213	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
108	107	3imp1 1201	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
109	108	anim2d 565	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
110	109	reximdva 2934	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
111	110	3adant2l 1213	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
112	111	3adant3r 1216	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
113	47, 112	mpd 15	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
114	113	3expia 1190	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
115	114	expd 436	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
116	115	reximdvai 2932	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
117	34, 116	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
118	117	3exp1 1204	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
119	118	imp 429	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
120	119	rexlimdv 2946	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
121	120	rexlimdvva 2954	. 2 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
122	5, 121	mpd 15	1 $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1370

wcel 1758

wrex 2800 class class class wbr 4401

cfv 5527 (class class class)co 6201

cbs 14293

cple 14365

cpo 15230

cplt 15231

cjn 15234

cp0 15327

cp1 15328

clat 15335

cops 33156

col 33158

ccvr 33246

catm 33247

chlt 33334

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4512 ax-sep 4522 ax-nul 4530 ax-pow 4579 ax-pr 4640 ax-un 6483

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-reu 2806 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-nul 3747 df-if 3901 df-pw 3971 df-sn 3987 df-pr 3989 df-op 3993 df-uni 4201 df-iun 4282 df-br 4402 df-opab 4460 df-mpt 4461 df-id 4745 df-xp 4955 df-rel 4956 df-cnv 4957 df-co 4958 df-dm 4959 df-rn 4960 df-res 4961 df-ima 4962 df-iota 5490 df-fun 5529 df-fn 5530 df-f 5531 df-f1 5532 df-fo 5533 df-f1o 5534 df-fv 5535 df-riota 6162 df-ov 6204 df-oprab 6205 df-poset 15236 df-plt 15248 df-lub 15264 df-glb 15265 df-join 15266 df-meet 15267 df-p0 15329 df-p1 15330 df-lat 15336 df-clat 15398 df-oposet 33160 df-ol 33162 df-oml 33163 df-covers 33250 df-ats 33251 df-atl 33282 df-cvlat 33306 df-hlat 33335

This theorem is referenced by: 3dim0 33440

W3C validator