Theorem iscvlat 39312

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 6822	. . . 4 ⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾))
2		iscvlat.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
3	1, 2	eqtr4di 2782	. . 3 ⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴)
4		fveq2 6822	. . . . . 6 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
5		iscvlat.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
6	4, 5	eqtr4di 2782	. . . . 5 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵)
7		fveq2 6822	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
8		iscvlat.l	. . . . . . . . . 10 ⊢ ≤ = (le‘𝐾)
9	7, 8	eqtr4di 2782	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ )
10	9	breqd 5103	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝑝(le‘𝑘)𝑥 ↔ 𝑝 ≤ 𝑥))
11	10	notbid 318	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (¬ 𝑝(le‘𝑘)𝑥 ↔ ¬ 𝑝 ≤ 𝑥))
12		eqidd 2730	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → 𝑝 = 𝑝)
13		fveq2 6822	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾))
14		iscvlat.j	. . . . . . . . . 10 ⊢ ∨ = (join‘𝐾)
15	13, 14	eqtr4di 2782	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ )
16	15	oveqd 7366	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝑥(join‘𝑘)𝑞) = (𝑥 ∨ 𝑞))
17	12, 9, 16	breq123d 5106	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞) ↔ 𝑝 ≤ (𝑥 ∨ 𝑞)))
18	11, 17	anbi12d 632	. . . . . 6 ⊢ (𝑘 = 𝐾 → ((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) ↔ (¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞))))
19		eqidd 2730	. . . . . . 7 ⊢ (𝑘 = 𝐾 → 𝑞 = 𝑞)
20	15	oveqd 7366	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑥(join‘𝑘)𝑝) = (𝑥 ∨ 𝑝))
21	19, 9, 20	breq123d 5106	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝) ↔ 𝑞 ≤ (𝑥 ∨ 𝑝)))
22	18, 21	imbi12d 344	. . . . 5 ⊢ (𝑘 = 𝐾 → (((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) → 𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝)) ↔ ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
23	6, 22	raleqbidv 3309	. . . 4 ⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Base‘𝑘)((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) → 𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝)) ↔ ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
24	3, 23	raleqbidv 3309	. . 3 ⊢ (𝑘 = 𝐾 → (∀𝑞 ∈ (Atoms‘𝑘)∀𝑥 ∈ (Base‘𝑘)((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) → 𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝)) ↔ ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
25	3, 24	raleqbidv 3309	. 2 ⊢ (𝑘 = 𝐾 → (∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)∀𝑥 ∈ (Base‘𝑘)((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) → 𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝)) ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
26		df-cvlat 39311	. 2 ⊢ CvLat = {𝑘 ∈ AtLat ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)∀𝑥 ∈ (Base‘𝑘)((¬ 𝑝(le‘𝑘)𝑥 ∧ 𝑝(le‘𝑘)(𝑥(join‘𝑘)𝑞)) → 𝑞(le‘𝑘)(𝑥(join‘𝑘)𝑝))}
27	25, 26	elrab2 3651	1 ⊢ (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044   class class class wbr 5092  ‘cfv 6482  (class class class)co 7349  Basecbs 17120  lecple 17168  joincjn 18217  Atomscatm 39252  AtLatcal 39253  CvLatclc 39254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-cvlat 39311

This theorem is referenced by:  iscvlat2N  39313  cvlatl  39314  cvlexch1  39317  ishlat2  39342