Theorem omlfh1N 38622

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 31343 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 38606	. . . . 5 ⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat)
2		omlfh1.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
3		eqid 2724	. . . . . 6 ⊢ (le‘𝐾) = (le‘𝐾)
4		omlfh1.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
5		omlfh1.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
6	2, 3, 4, 5	latledi 18434	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)))
7	1, 6	sylan 579	. . . 4 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)))
8	7	3adant3 1129	. . 3 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)))
9	1	adantr 480	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
10		simpr1 1191	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
11		simpr2 1192	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
12		simpr3 1193	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
13	2, 4	latjcl 18396	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 ∨ 𝑍) ∈ 𝐵)
14	9, 11, 12, 13	syl3anc 1368	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∨ 𝑍) ∈ 𝐵)
15	2, 5	latmcom 18420	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∨ 𝑍) ∈ 𝐵) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑌 ∨ 𝑍) ∧ 𝑋))
16	9, 10, 14, 15	syl3anc 1368	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑌 ∨ 𝑍) ∧ 𝑋))
17		omlol 38604	. . . . . . . . 9 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
18	17	adantr 480	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ OL)
19	2, 5	latmcl 18397	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)
20	9, 10, 11, 19	syl3anc 1368	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ∈ 𝐵)
21	2, 5	latmcl 18397	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 ∧ 𝑍) ∈ 𝐵)
22	9, 10, 12, 21	syl3anc 1368	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑍) ∈ 𝐵)
23		eqid 2724	. . . . . . . . 9 ⊢ (oc‘𝐾) = (oc‘𝐾)
24	2, 4, 5, 23	oldmj1 38585	. . . . . . . 8 ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑍) ∈ 𝐵) → ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) = (((oc‘𝐾)‘(𝑋 ∧ 𝑌)) ∧ ((oc‘𝐾)‘(𝑋 ∧ 𝑍))))
25	18, 20, 22, 24	syl3anc 1368	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) = (((oc‘𝐾)‘(𝑋 ∧ 𝑌)) ∧ ((oc‘𝐾)‘(𝑋 ∧ 𝑍))))
26	2, 4, 5, 23	oldmm1 38581	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∧ 𝑌)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)))
27	18, 10, 11, 26	syl3anc 1368	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘(𝑋 ∧ 𝑌)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)))
28	2, 4, 5, 23	oldmm1 38581	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∧ 𝑍)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))
29	18, 10, 12, 28	syl3anc 1368	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘(𝑋 ∧ 𝑍)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))
30	27, 29	oveq12d 7420	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((oc‘𝐾)‘(𝑋 ∧ 𝑌)) ∧ ((oc‘𝐾)‘(𝑋 ∧ 𝑍))) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))
31	25, 30	eqtrd 2764	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))
32	16, 31	oveq12d 7420	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))))
33	32	3adant3 1129	. . . 4 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))))
34		omlop 38605	. . . . . . . . . . 11 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OP)
35	34	adantr 480	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ OP)
36	2, 23	opoccl 38558	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
37	35, 10, 36	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
38	2, 23	opoccl 38558	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
39	35, 11, 38	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
40	2, 4	latjcl 18396	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
41	9, 37, 39, 40	syl3anc 1368	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
42	2, 23	opoccl 38558	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑍 ∈ 𝐵) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
43	35, 12, 42	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
44	2, 4	latjcl 18396	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
45	9, 37, 43, 44	syl3anc 1368	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
46	2, 5	latmcl 18397	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)) ∈ 𝐵) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) ∈ 𝐵)
47	9, 41, 45, 46	syl3anc 1368	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) ∈ 𝐵)
48	2, 5	latmassOLD 38593	. . . . . . 7 ⊢ ((𝐾 ∈ OL ∧ ((𝑌 ∨ 𝑍) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) ∈ 𝐵)) → (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))))
49	18, 14, 10, 47, 48	syl13anc 1369	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))))
50	49	3adant3 1129	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))))
51		omlfh1.c	. . . . . . . . . . . . . 14 ⊢ 𝐶 = (cm‘𝐾)
52	2, 23, 51	cmt2N 38614	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶((oc‘𝐾)‘𝑌)))
53	52	3adant3r3 1181	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶𝑌 ↔ 𝑋𝐶((oc‘𝐾)‘𝑌)))
54		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ OML)
55	2, 4, 5, 23, 51	cmtbr3N 38618	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (𝑋𝐶((oc‘𝐾)‘𝑌) ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌))))
56	54, 10, 39, 55	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶((oc‘𝐾)‘𝑌) ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌))))
57	53, 56	bitrd 279	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌))))
58	57	biimpa 476	. . . . . . . . . 10 ⊢ (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑋𝐶𝑌) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌)))
59	58	adantrr 714	. . . . . . . . 9 ⊢ (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌)))
60	59	3impa 1107	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) = (𝑋 ∧ ((oc‘𝐾)‘𝑌)))
61	2, 23, 51	cmt2N 38614	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋𝐶𝑍 ↔ 𝑋𝐶((oc‘𝐾)‘𝑍)))
62	61	3adant3r2 1180	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶𝑍 ↔ 𝑋𝐶((oc‘𝐾)‘𝑍)))
63	2, 4, 5, 23, 51	cmtbr3N 38618	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (𝑋𝐶((oc‘𝐾)‘𝑍) ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
64	54, 10, 43, 63	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶((oc‘𝐾)‘𝑍) ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
65	62, 64	bitrd 279	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋𝐶𝑍 ↔ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
66	65	biimpa 476	. . . . . . . . . 10 ⊢ (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑋𝐶𝑍) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍)))
67	66	adantrl 713	. . . . . . . . 9 ⊢ (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍)))
68	67	3impa 1107	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))) = (𝑋 ∧ ((oc‘𝐾)‘𝑍)))
69	60, 68	oveq12d 7420	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑋 ∧ ((oc‘𝐾)‘𝑌)) ∧ (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
70	2, 5	latmmdiN 38598	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)) → (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))))
71	18, 10, 41, 45, 70	syl13anc 1369	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))))
72	71	3adant3 1129	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = ((𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))))
73	2, 5	latmmdiN 38598	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵)) → (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))) = ((𝑋 ∧ ((oc‘𝐾)‘𝑌)) ∧ (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
74	18, 10, 39, 43, 73	syl13anc 1369	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))) = ((𝑋 ∧ ((oc‘𝐾)‘𝑌)) ∧ (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
75	74	3adant3 1129	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))) = ((𝑋 ∧ ((oc‘𝐾)‘𝑌)) ∧ (𝑋 ∧ ((oc‘𝐾)‘𝑍))))
76	69, 72, 75	3eqtr4d 2774	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))))
77	76	oveq2d 7418	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍))))) = ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))))
78	2, 5	latmcl 18397	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
79	9, 39, 43, 78	syl3anc 1368	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
80	2, 5	latm12 38594	. . . . . . 7 ⊢ ((𝐾 ∈ OL ∧ ((𝑌 ∨ 𝑍) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)) ∈ 𝐵)) → ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))))
81	18, 14, 10, 79, 80	syl13anc 1369	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))))
82	81	3adant3 1129	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑌 ∨ 𝑍) ∧ (𝑋 ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))))
83	50, 77, 82	3eqtrd 2768	. . . 4 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (((𝑌 ∨ 𝑍) ∧ 𝑋) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))))
84	2, 4, 5, 23	oldmj1 38585	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OL ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((oc‘𝐾)‘(𝑌 ∨ 𝑍)) = (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))
85	18, 11, 12, 84	syl3anc 1368	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((oc‘𝐾)‘(𝑌 ∨ 𝑍)) = (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))
86	85	oveq2d 7418	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 ∨ 𝑍) ∧ ((oc‘𝐾)‘(𝑌 ∨ 𝑍))) = ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))))
87		eqid 2724	. . . . . . . . . 10 ⊢ (0.‘𝐾) = (0.‘𝐾)
88	2, 23, 5, 87	opnoncon 38572	. . . . . . . . 9 ⊢ ((𝐾 ∈ OP ∧ (𝑌 ∨ 𝑍) ∈ 𝐵) → ((𝑌 ∨ 𝑍) ∧ ((oc‘𝐾)‘(𝑌 ∨ 𝑍))) = (0.‘𝐾))
89	35, 14, 88	syl2anc 583	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 ∨ 𝑍) ∧ ((oc‘𝐾)‘(𝑌 ∨ 𝑍))) = (0.‘𝐾))
90	86, 89	eqtr3d 2766	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍))) = (0.‘𝐾))
91	90	oveq2d 7418	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (𝑋 ∧ (0.‘𝐾)))
92	2, 5, 87	olm01 38600	. . . . . . 7 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ (0.‘𝐾)) = (0.‘𝐾))
93	18, 10, 92	syl2anc 583	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (0.‘𝐾)) = (0.‘𝐾))
94	91, 93	eqtrd 2764	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (0.‘𝐾))
95	94	3adant3 1129	. . . 4 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ ((𝑌 ∨ 𝑍) ∧ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑍)))) = (0.‘𝐾))
96	33, 83, 95	3eqtrd 2768	. . 3 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (0.‘𝐾))
97	2, 4	latjcl 18396	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑍) ∈ 𝐵) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐵)
98	9, 20, 22, 97	syl3anc 1368	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐵)
99	2, 5	latmcl 18397	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∨ 𝑍) ∈ 𝐵) → (𝑋 ∧ (𝑌 ∨ 𝑍)) ∈ 𝐵)
100	9, 10, 14, 99	syl3anc 1368	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) ∈ 𝐵)
101	2, 3, 5, 23, 87	omllaw3 38609	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐵 ∧ (𝑋 ∧ (𝑌 ∨ 𝑍)) ∈ 𝐵) → ((((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (0.‘𝐾)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (𝑌 ∨ 𝑍))))
102	54, 98, 100, 101	syl3anc 1368	. . . 4 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (0.‘𝐾)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (𝑌 ∨ 𝑍))))
103	102	3adant3 1129	. . 3 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))(le‘𝐾)(𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((𝑋 ∧ (𝑌 ∨ 𝑍)) ∧ ((oc‘𝐾)‘((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))) = (0.‘𝐾)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (𝑌 ∨ 𝑍))))
104	8, 96, 103	mp2and 696	. 2 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (𝑌 ∨ 𝑍)))
105	104	eqcomd 2730	1 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   class class class wbr 5139  ‘cfv 6534  (class class class)co 7402  Basecbs 17145  lecple 17205  occoc 17206  joincjn 18268  meetcmee 18269  0.cp0 18380  Latclat 18388  OPcops 38536  cmccmtN 38537  OLcol 38538  OMLcoml 38539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-proset 18252  df-poset 18270  df-lub 18303  df-glb 18304  df-join 18305  df-meet 18306  df-p0 18382  df-lat 18389  df-oposet 38540  df-cmtN 38541  df-ol 38542  df-oml 38543

This theorem is referenced by:  omlfh3N  38623  omlmod1i2N  38624