Theorem iscvlat 40294

Description: The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.)

Hypotheses

Ref	Expression
iscvlat.b	⊢ 𝐵 = (Base‘𝐾)
iscvlat.l	⊢ ≤ = (le‘𝐾)
iscvlat.j	⊢ ∨ = (join‘𝐾)
iscvlat.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
iscvlat	⊢ (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))

Distinct variable groups:   𝑞,𝑝,𝐴   𝑥,𝐵   𝑥,𝑝,𝐾,𝑞

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑞, 𝑝)   ∨ (𝑥, 𝑞, 𝑝)   ≤ (𝑥, 𝑞, 𝑝)

Proof of Theorem iscvlat

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6874	. . . 4 ⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾))
2		iscvlat.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
3	1, 2	eqtr4di 2813	. . 3 ⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴)
4		fveq2 6874	. . . . . 6 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
5		iscvlat.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
6	4, 5	eqtr4di 2813	. . . . 5 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵)
7		fveq2 6874	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
8		iscvlat.l	. . . . . . . . . 10 ⊢ ≤ = (le‘𝐾)
9	7, 8	eqtr4di 2813	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ )
10	9	breqd 5114	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝑝(le‘𝑘)𝑥 ↔ 𝑝 ≤ 𝑥))
11	10	notbid 321	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (¬ 𝑝(le‘𝑘)𝑥 ↔ ¬ 𝑝 ≤ 𝑥))
12		eqidd 2761	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → 𝑝 = 𝑝)
13		fveq2 6874	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾))
14		iscvlat.j	. . . . . . . . . 10 ⊢ ∨ = (join‘𝐾)
15	13, 14	eqtr4di 2813	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ )
16	15	oveqd 7426	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝑥(join‘𝑘)𝑞) = (𝑥 ∨ 𝑞))
17	12, 9, 16	breq123d 5117	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞) ↔ 𝑝 ≤ (𝑥 ∨ 𝑞)))
18	11, 17	anbi12d 644	. . . . . 6 ⊢ (𝑘 = 𝐾 → ((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) ↔ (¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞))))
19		eqidd 2761	. . . . . . 7 ⊢ (𝑘 = 𝐾 → 𝑞 = 𝑞)
20	15	oveqd 7426	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑥(join‘𝑘)𝑝) = (𝑥 ∨ 𝑝))
21	19, 9, 20	breq123d 5117	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝) ↔ 𝑞 ≤ (𝑥 ∨ 𝑝)))
22	18, 21	imbi12d 347	. . . . 5 ⊢ (𝑘 = 𝐾 → (((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) → 𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝)) ↔ ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
23	6, 22	raleqbidv 3334	. . . 4 ⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Base‘𝑘)((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) → 𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝)) ↔ ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
24	3, 23	raleqbidv 3334	. . 3 ⊢ (𝑘 = 𝐾 → (∀𝑞 ∈ (Atoms‘𝑘)∀𝑥 ∈ (Base‘𝑘)((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) → 𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝)) ↔ ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
25	3, 24	raleqbidv 3334	. 2 ⊢ (𝑘 = 𝐾 → (∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)∀𝑥 ∈ (Base‘𝑘)((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) → 𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝)) ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
26		df-cvlat 40293	. 2 ⊢ CvLat = {𝑘 ∈ AtLat ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)∀𝑥 ∈ (Base‘𝑘)((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) → 𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝))}
27	25, 26	elrab2 3649	1 ⊢ (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076   class class class wbr 5103  ‘cfv 6528  (class class class)co 7409  Basecbs 17334  lecple 17382  joincjn 18432  Atomscatm 40234  AtLatcal 40235  CvLatclc 40236

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6484  df-fv 6536  df-ov 7412  df-cvlat 40293

This theorem is used by:  iscvlat2N  40295  cvlatl  40296  cvlexch1  40299  ishlat2  40324