Theorem omlfh1N 40235

Description: Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in [Kalmbach] p. 25. (fh1 32153 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
omlfh1.b	⊢ 𝐵 = (Base‘𝐾)
omlfh1.j	⊢ ∨ = (join‘𝐾)
omlfh1.m	⊢ ∧ = (meet‘𝐾)
omlfh1.c	⊢ 𝐶 = (cm‘𝐾)

Assertion

Ref	Expression
omlfh1N	⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))

Proof of Theorem omlfh1N

Step	Hyp	Ref	Expression
1		omllat 40219	. . . . 5 ⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat)
2		omlfh1.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
3		eqid 2760	. . . . . 6 ⊢ (le‘𝐾) = (le‘𝐾)
4		omlfh1.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
5		omlfh1.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
6	2, 3, 4, 5	latledi 18612	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)))
7	1, 6	sylan 592	. . . 4 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)))
8	7	3adant3 1150	. . 3 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)))
9	1	adantr 486	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
10		simpr1 1213	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
11		simpr2 1214	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
12		simpr3 1215	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
13	2, 4	latjcl 18574	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 ∨ 𝑍) ∈ 𝐵)
14	9, 11, 12, 13	syl3anc 1398	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∨ 𝑍) ∈ 𝐵)
15	2, 5	latmcom 18598	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∨ 𝑍) ∈ 𝐵) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑌 ∨ 𝑍) ∧ 𝑋))
16	9, 10, 14, 15	syl3anc 1398	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑌 ∨ 𝑍) ∧ 𝑋))
17		omlol 40217	. . . . . . . . 9 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
18	17	adantr 486	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ OL)
19	2, 5	latmcl 18575	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)
20	9, 10, 11, 19	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ∈ 𝐵)
21	2, 5	latmcl 18575	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 ∧ 𝑍) ∈ 𝐵)
22	9, 10, 12, 21	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑍) ∈ 𝐵)
23		eqid 2760	. . . . . . . . 9 ⊢ (oc‘𝐾) = (oc‘𝐾)
24	2, 4, 5, 23	oldmj1 40198	. . . . . . . 8 ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑍) ∈ 𝐵) → ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) = (((oc‘𝐾)‘(𝑋 ∧ 𝑌)) ∧ ((oc‘𝐾)‘(𝑋 ∧ 𝑍))))
25	18, 20, 22, 24	syl3anc 1398	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) = (((oc‘𝐾)‘(𝑋 ∧ 𝑌)) ∧ ((oc‘𝐾)‘(𝑋 ∧ 𝑍))))
26	2, 4, 5, 23	oldmm1 40194	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∧ 𝑌)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)))
27	18, 10, 11, 26	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘(𝑋 ∧ 𝑌)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)))
28	2, 4, 5, 23	oldmm1 40194	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∧ 𝑍)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))
29	18, 10, 12, 28	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘(𝑋 ∧ 𝑍)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))
30	27, 29	oveq12d 7426	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((oc‘𝐾)‘(𝑋 ∧ 𝑌)) ∧ ((oc‘𝐾)‘(𝑋 ∧ 𝑍))) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))
31	25, 30	eqtrd 2795	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))
32	16, 31	oveq12d 7426	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))))
33	32	3adant3 1150	. . . 4 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))))
34		omlop 40218	. . . . . . . . . . 11 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OP)
35	34	adantr 486	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ OP)
36	2, 23	opoccl 40171	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
37	35, 10, 36	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
38	2, 23	opoccl 40171	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
39	35, 11, 38	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
40	2, 4	latjcl 18574	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
41	9, 37, 39, 40	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
42	2, 23	opoccl 40171	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑍 ∈ 𝐵) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
43	35, 12, 42	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
44	2, 4	latjcl 18574	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
45	9, 37, 43, 44	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
46	2, 5	latmcl 18575	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)) ∈ 𝐵) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) ∈ 𝐵)
47	9, 41, 45, 46	syl3anc 1398	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) ∈ 𝐵)
48	2, 5	latmassOLD 40206	. . . . . . 7 ⊢ ((𝐾 ∈ OL ∧ ((𝑌 ∨ 𝑍) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) ∈ 𝐵)) → (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))))
49	18, 14, 10, 47, 48	syl13anc 1399	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))))
50	49	3adant3 1150	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))))
51		omlfh1.c	. . . . . . . . . . . . . 14 ⊢ 𝐶 = (cm‘𝐾)
52	2, 23, 51	cmt2N 40227	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶((oc‘𝐾)‘𝑌)))
53	52	3adant3r3 1203	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶𝑌 ↔ 𝑋𝐶((oc‘𝐾)‘𝑌)))
54		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ OML)
55	2, 4, 5, 23, 51	cmtbr3N 40231	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (𝑋𝐶((oc‘𝐾)‘𝑌) ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌))))
56	54, 10, 39, 55	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶((oc‘𝐾)‘𝑌) ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌))))
57	53, 56	bitrd 282	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌))))
58	57	biimpa 482	. . . . . . . . . 10 ⊢ (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑋𝐶𝑌) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌)))
59	58	adantrr 730	. . . . . . . . 9 ⊢ (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌)))
60	59	3impa 1127	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌)))
61	2, 23, 51	cmt2N 40227	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋𝐶𝑍 ↔ 𝑋𝐶((oc‘𝐾)‘𝑍)))
62	61	3adant3r2 1202	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶𝑍 ↔ 𝑋𝐶((oc‘𝐾)‘𝑍)))
63	2, 4, 5, 23, 51	cmtbr3N 40231	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (𝑋𝐶((oc‘𝐾)‘𝑍) ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
64	54, 10, 43, 63	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶((oc‘𝐾)‘𝑍) ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
65	62, 64	bitrd 282	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶𝑍 ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
66	65	biimpa 482	. . . . . . . . . 10 ⊢ (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑋𝐶𝑍) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍)))
67	66	adantrl 729	. . . . . . . . 9 ⊢ (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍)))
68	67	3impa 1127	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍)))
69	60, 68	oveq12d 7426	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑋 ∧ ((oc‘𝐾)‘𝑌)) ∧ (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
70	2, 5	latmmdiN 40211	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)) → (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))))
71	18, 10, 41, 45, 70	syl13anc 1399	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))))
72	71	3adant3 1150	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))))
73	2, 5	latmmdiN 40211	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵)) → (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))) = ((𝑋 ∧ ((oc‘𝐾)‘𝑌)) ∧ (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
74	18, 10, 39, 43, 73	syl13anc 1399	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))) = ((𝑋 ∧ ((oc‘𝐾)‘𝑌)) ∧ (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
75	74	3adant3 1150	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))) = ((𝑋 ∧ ((oc‘𝐾)‘𝑌)) ∧ (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
76	69, 72, 75	3eqtr4d 2805	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))))
77	76	oveq2d 7424	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))) = ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))))
78	2, 5	latmcl 18575	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
79	9, 39, 43, 78	syl3anc 1398	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
80	2, 5	latm12 40207	. . . . . . 7 ⊢ ((𝐾 ∈ OL ∧ ((𝑌 ∨ 𝑍) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)) → ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))))
81	18, 14, 10, 79, 80	syl13anc 1399	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))))
82	81	3adant3 1150	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))))
83	50, 77, 82	3eqtrd 2799	. . . 4 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))))
84	2, 4, 5, 23	oldmj1 40198	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OL ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((oc‘𝐾)‘(𝑌 ∨ 𝑍)) = (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))
85	18, 11, 12, 84	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘(𝑌 ∨ 𝑍)) = (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))
86	85	oveq2d 7424	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 ∨ 𝑍) ∧ ((oc‘𝐾)‘(𝑌 ∨ 𝑍))) = ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))))
87		eqid 2760	. . . . . . . . . 10 ⊢ (0.‘𝐾) = (0.‘𝐾)
88	2, 23, 5, 87	opnoncon 40185	. . . . . . . . 9 ⊢ ((𝐾 ∈ OP ∧ (𝑌 ∨ 𝑍) ∈ 𝐵) → ((𝑌 ∨ 𝑍) ∧ ((oc‘𝐾)‘(𝑌 ∨ 𝑍))) = (0.‘𝐾))
89	35, 14, 88	syl2anc 596	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 ∨ 𝑍) ∧ ((oc‘𝐾)‘(𝑌 ∨ 𝑍))) = (0.‘𝐾))
90	86, 89	eqtr3d 2797	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))) = (0.‘𝐾))
91	90	oveq2d 7424	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ (0.‘𝐾)))
92	2, 5, 87	olm01 40213	. . . . . . 7 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ (0.‘𝐾)) = (0.‘𝐾))
93	18, 10, 92	syl2anc 596	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (0.‘𝐾)) = (0.‘𝐾))
94	91, 93	eqtrd 2795	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (0.‘𝐾))
95	94	3adant3 1150	. . . 4 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (0.‘𝐾))
96	33, 83, 95	3eqtrd 2799	. . 3 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (0.‘𝐾))
97	2, 4	latjcl 18574	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑍) ∈ 𝐵) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐵)
98	9, 20, 22, 97	syl3anc 1398	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐵)
99	2, 5	latmcl 18575	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∨ 𝑍) ∈ 𝐵) → (𝑋 ∧ (𝑌 ∨ 𝑍)) ∈ 𝐵)
100	9, 10, 14, 99	syl3anc 1398	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) ∈ 𝐵)
101	2, 3, 5, 23, 87	omllaw3 40222	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐵 ∧ (𝑋 ∧ (𝑌 ∨ 𝑍)) ∈ 𝐵) → ((((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (0.‘𝐾)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (𝑌 ∨ 𝑍))))
102	54, 98, 100, 101	syl3anc 1398	. . . 4 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (0.‘𝐾)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (𝑌 ∨ 𝑍))))
103	102	3adant3 1150	. . 3 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (0.‘𝐾)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (𝑌 ∨ 𝑍))))
104	8, 96, 103	mp2and 712	. 2 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (𝑌 ∨ 𝑍)))
105	104	eqcomd 2766	1 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   class class class wbr 5102  ‘cfv 6527  (class class class)co 7408  Basecbs 17348  lecple 17396  occoc 17397  joincjn 18446  meetcmee 18447  0.cp0 18556  Latclat 18566  OPcops 40149  cmccmtN 40150  OLcol 40151  OMLcoml 40152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-proset 18429  df-poset 18448  df-lub 18479  df-glb 18480  df-join 18481  df-meet 18482  df-p0 18558  df-lat 18567  df-oposet 40153  df-cmtN 40154  df-ol 40155  df-oml 40156

This theorem is used by:  omlfh3N  40236  omlmod1i2N  40237