cmtbr3N - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cmtbr3N		Structured version Visualization version GIF version

Theorem cmtbr3N 40311

Description: Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (cmbr3 32210 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
cmtbr2.b	⊢ 𝐵 = (Base‘𝐾)
cmtbr2.j	⊢ ∨ = (join‘𝐾)
cmtbr2.m	⊢ ∧ = (meet‘𝐾)
cmtbr2.o	⊢ ⊥ = (oc‘𝐾)
cmtbr2.c	⊢ 𝐶 = (cm‘𝐾)

**Assertion**
Ref	Expression
cmtbr3N	⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))

**Proof of Theorem cmtbr3N**
Step	Hyp	Ref	Expression
1		cmtbr2.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
2		cmtbr2.c	. . . . 5 ⊢ 𝐶 = (cm‘𝐾)
3	1, 2	cmtcomN 40306	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑌𝐶𝑋))
4		cmtbr2.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
5		cmtbr2.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
6		cmtbr2.o	. . . . . 6 ⊢ ⊥ = (oc‘𝐾)
7	1, 4, 5, 6, 2	cmtbr2N 40310	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌𝐶𝑋 ↔ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
8	7	3com23 1144	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌𝐶𝑋 ↔ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
9	3, 8	bitrd 282	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
10		oveq2 7428	. . . . . 6 ⊢ (𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋))) → (𝑋 ∧ 𝑌) = (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
11	10	adantl 487	. . . . 5 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))) → (𝑋 ∧ 𝑌) = (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
12		omlol 40297	. . . . . . . . 9 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
13	12	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OL)
14		simp2 1155	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
15		omllat 40299	. . . . . . . . . 10 ⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat)
16	15	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
17		simp3 1156	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
18	1, 4	latjcl 18613	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌 ∨ 𝑋) ∈ 𝐵)
19	16, 17, 14, 18	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 ∨ 𝑋) ∈ 𝐵)
20		omlop 40298	. . . . . . . . . . 11 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OP)
21	20	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP)
22	1, 6	opoccl 40251	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)
23	21, 14, 22	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)
24	1, 4	latjcl 18613	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ ( ⊥ ‘𝑋) ∈ 𝐵) → (𝑌 ∨ ( ⊥ ‘𝑋)) ∈ 𝐵)
25	16, 17, 23, 24	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 ∨ ( ⊥ ‘𝑋)) ∈ 𝐵)
26	1, 5	latmassOLD 40286	. . . . . . . 8 ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ (𝑌 ∨ 𝑋) ∈ 𝐵 ∧ (𝑌 ∨ ( ⊥ ‘𝑋)) ∈ 𝐵)) → ((𝑋 ∧ (𝑌 ∨ 𝑋)) ∧ (𝑌 ∨ ( ⊥ ‘𝑋))) = (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
27	13, 14, 19, 25, 26	syl13anc 1399	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (𝑌 ∨ 𝑋)) ∧ (𝑌 ∨ ( ⊥ ‘𝑋))) = (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
28	1, 4	latjcom 18621	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌 ∨ 𝑋) = (𝑋 ∨ 𝑌))
29	16, 17, 14, 28	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 ∨ 𝑋) = (𝑋 ∨ 𝑌))
30	29	oveq2d 7436	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑌 ∨ 𝑋)) = (𝑋 ∧ (𝑋 ∨ 𝑌)))
31	1, 4, 5	latabs2 18650	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑋 ∨ 𝑌)) = 𝑋)
32	15, 31	syl3an1 1181	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑋 ∨ 𝑌)) = 𝑋)
33	30, 32	eqtrd 2796	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑌 ∨ 𝑋)) = 𝑋)
34	1, 4	latjcom 18621	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ ( ⊥ ‘𝑋) ∈ 𝐵) → (𝑌 ∨ ( ⊥ ‘𝑋)) = (( ⊥ ‘𝑋) ∨ 𝑌))
35	16, 17, 23, 34	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 ∨ ( ⊥ ‘𝑋)) = (( ⊥ ‘𝑋) ∨ 𝑌))
36	33, 35	oveq12d 7438	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (𝑌 ∨ 𝑋)) ∧ (𝑌 ∨ ( ⊥ ‘𝑋))) = (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)))
37	27, 36	eqtr3d 2798	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))) = (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)))
38	37	adantr 486	. . . . 5 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))) → (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))) = (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)))
39	11, 38	eqtr2d 2797	. . . 4 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))) → (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌))
40	39	ex 418	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋))) → (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))
41	9, 40	sylbid 243	. 2 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 → (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))
42		simp1 1154	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OML)
43	1, 6	opoccl 40251	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵)
44	21, 17, 43	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵)
45	1, 5	latmcl 18614	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵)
46	16, 14, 44, 45	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵)
47	42, 46, 14	3jca 1146	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐾 ∈ OML ∧ (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵))
48		eqid 2761	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
49	1, 48, 5	latmle1 18638	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑌))(le‘𝐾)𝑋)
50	16, 14, 44, 49	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑌))(le‘𝐾)𝑋)
51	1, 48, 4, 5, 6	omllaw2N 40301	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝑋 ∧ ( ⊥ ‘𝑌))(le‘𝐾)𝑋 → ((𝑋 ∧ ( ⊥ ‘𝑌)) ∨ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋)) = 𝑋))
52	47, 50, 51	sylc 66	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ ( ⊥ ‘𝑌)) ∨ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋)) = 𝑋)
53	1, 6	opoccl 40251	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∈ 𝐵)
54	21, 46, 53	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∈ 𝐵)
55	1, 5	latmcl 18614	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∈ 𝐵)
56	16, 54, 14, 55	syl3anc 1398	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∈ 𝐵)
57	1, 4	latjcom 18621	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵 ∧ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∈ 𝐵) → ((𝑋 ∧ ( ⊥ ‘𝑌)) ∨ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋)) = ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
58	16, 46, 56, 57	syl3anc 1398	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ ( ⊥ ‘𝑌)) ∨ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋)) = ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
59	52, 58	eqtr3d 2798	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 = ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
60	59	adantr 486	. . . . 5 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)) → 𝑋 = ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
61	1, 4, 5, 6	oldmm3N 40276	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∨ 𝑌))
62	12, 61	syl3an1 1181	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∨ 𝑌))
63	62	oveq2d 7436	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌)))) = (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)))
64	1, 5	latmcom 18637	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌)))) = (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋))
65	16, 14, 54, 64	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌)))) = (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋))
66	63, 65	eqtr3d 2798	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋))
67	66	eqeq1d 2763	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌) ↔ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) = (𝑋 ∧ 𝑌)))
68		oveq1 7427	. . . . . . 7 ⊢ ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) = (𝑋 ∧ 𝑌) → ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
69	67, 68	biimtrdi 256	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌) → ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌)))))
70	69	imp 412	. . . . 5 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)) → ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
71	60, 70	eqtrd 2796	. . . 4 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)) → 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
72	71	ex 418	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌) → 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌)))))
73	1, 4, 5, 6, 2	cmtvalN 40268	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌)))))
74	72, 73	sylibrd 262	. 2 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌) → 𝑋𝐶𝑌))
75	41, 74	impbid 215	1 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 class class class wbr 5103 ‘cfv 6538 (class class class)co 7420 Basecbs 17387 lecple 17435 occoc 17436 joincjn 18485 meetcmee 18486 Latclat 18605 OPcops 40229 cmccmtN 40230 OLcol 40231 OMLcoml 40232

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 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-proset 18468 df-poset 18487 df-lub 18518 df-glb 18519 df-join 18520 df-meet 18521 df-lat 18606 df-oposet 40233 df-cmtN 40234 df-ol 40235 df-oml 40236

This theorem is used by: cmtbr4N 40312 omlfh1N 40315

W3C validator