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 34127

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 2460	. . 3
2		eqid 2460	. . 3
3		eqid 2460	. . 3
4		eqid 2460	. . 3
5	1, 2, 3, 4	hlhgt4 34059	. 2 $/\$ $/\$ $/\$
6		simpl1 994	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		hlop 34034	. . . . . . . . . 10
8	1, 3	op0cl 33856	. . . . . . . . . 10
9	6, 7, 8	3syl 20	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simpl2l 1044	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		simprll 761	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		eqid 2460	. . . . . . . . . 10
13		athgt.j	. . . . . . . . . 10 $.\/$
14		athgt.c	. . . . . . . . . 10
15		athgt.a	. . . . . . . . . 10
16	1, 12, 2, 13, 14, 15	hlrelat3 34083	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
17	6, 9, 10, 11, 16	syl31anc 1226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
18		simp11 1021	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		simp3 993	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20	3, 14, 15	atcvr0 33960	. . . . . . . . . . . . . 14 $/\$
21	18, 19, 20	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		hlol 34033	. . . . . . . . . . . . . . 15
23	18, 22	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24	1, 15	atbase 33961	. . . . . . . . . . . . . . 15
25	24	3ad2ant3 1014	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	1, 13, 3	olj02 33898	. . . . . . . . . . . . . 14 $/\$ $.\/$
27	23, 25, 26	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
28	21, 27	breqtrrd 4466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29	28	biantrurd 508	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
30	27	breq1d 4450	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
31	29, 30	bitr3d 255	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
32	31	3expa 1191	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
33	32	rexbidva 2963	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
34	17, 33	mpbid 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		simp11 1021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36	25	3adant3r 1220	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		simp12r 1105	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		simp3r 1020	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		simp2lr 1059	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		hlpos 34037	. . . . . . . . . . . . . . 15
41	35, 40	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simp12l 1104	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	1, 12, 2	plelttr 15448	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
44	41, 36, 42, 37, 43	syl13anc 1225	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	38, 39, 44	mp2and 679	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	1, 12, 2, 13, 14, 15	hlrelat3 34083	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
47	35, 36, 37, 45, 46	syl31anc 1226	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
48		simp11 1021	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49		hllat 34035	. . . . . . . . . . . . . . . . . . . . . . . 24
50	48, 49	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
51		simp3ll 1062	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
52	51, 24	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
53		simp3lr 1063	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
54	1, 15	atbase 33961	. . . . . . . . . . . . . . . . . . . . . . . 24
55	53, 54	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
56	1, 13	latjcl 15527	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $.\/$
57	50, 52, 55, 56	syl3anc 1223	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
58		simp13 1023	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
59		simp3r 1020	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
60		simp2l 1017	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
61	48, 40	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
62		simp12 1022	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
63	1, 12, 2	plelttr 15448	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
64	61, 57, 62, 58, 63	syl13anc 1225	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
65	59, 60, 64	mp2and 679	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
66	1, 12, 2, 13, 14, 15	hlrelat3 34083	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
67	48, 57, 58, 65, 66	syl31anc 1226	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
68		simp1ll 1054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
69	68, 49	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
70		simp2ll 1058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
71	70, 24	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
72		simp2lr 1059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
73	72, 54	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
74	69, 71, 73, 56	syl3anc 1223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
75		simp3l 1019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
76	1, 15	atbase 33961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77	75, 76	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
78	1, 13	latjcl 15527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $.\/$ $/\$ $.\/$ $.\/$
79	69, 74, 77, 78	syl3anc 1223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
80	1, 4	op1cl 33857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
81	68, 7, 80	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
82		simp3r 1020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
83		simp1r 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
84	68, 40	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
85		simp1lr 1055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
86	1, 12, 2	plelttr 15448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
87	84, 79, 85, 81, 86	syl13anc 1225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
88	82, 83, 87	mp2and 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
89	1, 12, 2, 13, 14, 15	hlrelat3 34083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
90	68, 79, 81, 88, 89	syl31anc 1226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
91		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
92	91	reximi 2925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
93	90, 92	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
94	93	3exp 1190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
95	94	exp4a 606	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
96	95	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
97	96	3adant2 1010	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
98	97	3imp 1185	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
99	98	3adant2l 1217	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
100	99	imp 429	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
101	100	anim2d 565	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
102	101	reximdva 2931	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
103	67, 102	mpd 15	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
104	103	3exp 1190	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
105	104	exp4a 606	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
106	105	exp4a 606	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
107	106	3adant2l 1217	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
108	107	3imp1 1204	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
109	108	anim2d 565	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
110	109	reximdva 2931	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
111	110	3adant2l 1217	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
112	111	3adant3r 1220	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
113	47, 112	mpd 15	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
114	113	3expia 1193	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
115	114	expd 436	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
116	115	reximdvai 2928	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
117	34, 116	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
118	117	3exp1 1207	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
119	118	imp 429	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
120	119	rexlimdv 2946	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
121	120	rexlimdvva 2955	. 2 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
122	5, 121	mpd 15	1 $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1374

wcel 1762

wrex 2808 class class class wbr 4440

cfv 5579 (class class class)co 6275

cbs 14479

cple 14551

cpo 15416

cplt 15417

cjn 15420

cp0 15513

cp1 15514

clat 15521

cops 33844

col 33846

ccvr 33934

catm 33935

chlt 34022

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-op 4027 df-uni 4239 df-iun 4320 df-br 4441 df-opab 4499 df-mpt 4500 df-id 4788 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-riota 6236 df-ov 6278 df-oprab 6279 df-poset 15422 df-plt 15434 df-lub 15450 df-glb 15451 df-join 15452 df-meet 15453 df-p0 15515 df-p1 15516 df-lat 15522 df-clat 15584 df-oposet 33848 df-ol 33850 df-oml 33851 df-covers 33938 df-ats 33939 df-atl 33970 df-cvlat 33994 df-hlat 34023

This theorem is referenced by: 3dim0 34128

W3C validator