Theorem isoml 40119

Description: The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011.)

Hypotheses

Ref	Expression
isoml.b	⊢ 𝐵 = (Base‘𝐾)
isoml.l	⊢ ≤ = (le‘𝐾)
isoml.j	⊢ ∨ = (join‘𝐾)
isoml.m	⊢ ∧ = (meet‘𝐾)
isoml.o	⊢ ⊥ = (oc‘𝐾)

Assertion

Ref	Expression
isoml	⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))

Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐾,𝑦

Allowed substitution hints:   ∨ (𝑥, 𝑦)   ≤ (𝑥, 𝑦)   ∧ (𝑥, 𝑦)   ⊥ (𝑥, 𝑦)

Proof of Theorem isoml

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6882	. . . 4 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
2		isoml.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
3	1, 2	eqtr4di 2815	. . 3 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵)
4		fveq2 6882	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
5		isoml.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
6	4, 5	eqtr4di 2815	. . . . . 6 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ )
7	6	breqd 5118	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝑥(le‘𝑘)𝑦 ↔ 𝑥 ≤ 𝑦))
8		fveq2 6882	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾))
9		isoml.j	. . . . . . . 8 ⊢ ∨ = (join‘𝐾)
10	8, 9	eqtr4di 2815	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ )
11		eqidd 2763	. . . . . . 7 ⊢ (𝑘 = 𝐾 → 𝑥 = 𝑥)
12		fveq2 6882	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾))
13		isoml.m	. . . . . . . . 9 ⊢ ∧ = (meet‘𝐾)
14	12, 13	eqtr4di 2815	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (meet‘𝑘) = ∧ )
15		eqidd 2763	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → 𝑦 = 𝑦)
16		fveq2 6882	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → (oc‘𝑘) = (oc‘𝐾))
17		isoml.o	. . . . . . . . . 10 ⊢ ⊥ = (oc‘𝐾)
18	16, 17	eqtr4di 2815	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (oc‘𝑘) = ⊥ )
19	18	fveq1d 6884	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → ((oc‘𝑘)‘𝑥) = ( ⊥ ‘𝑥))
20	14, 15, 19	oveq123d 7438	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)) = (𝑦 ∧ ( ⊥ ‘𝑥)))
21	10, 11, 20	oveq123d 7438	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))) = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))
22	21	eqeq2d 2773	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))) ↔ 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))
23	7, 22	imbi12d 347	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
24	3, 23	raleqbidv 3336	. . 3 ⊢ (𝑘 = 𝐾 → (∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
25	3, 24	raleqbidv 3336	. 2 ⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥)))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
26		df-oml 40060	. 2 ⊢ OML = {𝑘 ∈ OL ∣ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 → 𝑦 = (𝑥(join‘𝑘)(𝑦(meet‘𝑘)((oc‘𝑘)‘𝑥))))}
27	25, 26	elrab2 3652	1 ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078   class class class wbr 5107  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  lecple 17355  occoc 17356  joincjn 18405  meetcmee 18406  OLcol 40055  OMLcoml 40056

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-ext 2734

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-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-oml 40060

This theorem is used by:  isomliN  40120  omlol  40121  omllaw  40124