Theorem isatl 39275

Description: The predicate "is an atomic lattice." Every nonzero element is less than or equal to an atom. (Contributed by NM, 18-Sep-2011.) (Revised by NM, 14-Sep-2018.)

Hypotheses

Ref	Expression
isatlat.b	⊢ 𝐵 = (Base‘𝐾)
isatlat.g	⊢ 𝐺 = (glb‘𝐾)
isatlat.l	⊢ ≤ = (le‘𝐾)
isatlat.z	⊢ 0 = (0.‘𝐾)
isatlat.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
isatl	⊢ (𝐾 ∈ AtLat ↔ (𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)))

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

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑦)   𝐺(𝑥,𝑦)   ≤ (𝑥,𝑦)   0 (𝑥,𝑦)

Proof of Theorem isatl

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6886	. . . . . 6 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
2		isatlat.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
3	1, 2	eqtr4di 2787	. . . . 5 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵)
4		fveq2 6886	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (glb‘𝑘) = (glb‘𝐾))
5		isatlat.g	. . . . . . 7 ⊢ 𝐺 = (glb‘𝐾)
6	4, 5	eqtr4di 2787	. . . . . 6 ⊢ (𝑘 = 𝐾 → (glb‘𝑘) = 𝐺)
7	6	dmeqd 5896	. . . . 5 ⊢ (𝑘 = 𝐾 → dom (glb‘𝑘) = dom 𝐺)
8	3, 7	eleq12d 2827	. . . 4 ⊢ (𝑘 = 𝐾 → ((Base‘𝑘) ∈ dom (glb‘𝑘) ↔ 𝐵 ∈ dom 𝐺))
9		fveq2 6886	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (0.‘𝑘) = (0.‘𝐾))
10		isatlat.z	. . . . . . . 8 ⊢ 0 = (0.‘𝐾)
11	9, 10	eqtr4di 2787	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (0.‘𝑘) = 0 )
12	11	neeq2d 2991	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝑥 ≠ (0.‘𝑘) ↔ 𝑥 ≠ 0 ))
13		fveq2 6886	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾))
14		isatlat.a	. . . . . . . 8 ⊢ 𝐴 = (Atoms‘𝐾)
15	13, 14	eqtr4di 2787	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴)
16		fveq2 6886	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
17		isatlat.l	. . . . . . . . 9 ⊢ ≤ = (le‘𝐾)
18	16, 17	eqtr4di 2787	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ )
19	18	breqd 5134	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑦(le‘𝑘)𝑥 ↔ 𝑦 ≤ 𝑥))
20	15, 19	rexeqbidv 3330	. . . . . 6 ⊢ (𝑘 = 𝐾 → (∃𝑦 ∈ (Atoms‘𝑘)𝑦(le‘𝑘)𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))
21	12, 20	imbi12d 344	. . . . 5 ⊢ (𝑘 = 𝐾 → ((𝑥 ≠ (0.‘𝑘) → ∃𝑦 ∈ (Atoms‘𝑘)𝑦(le‘𝑘)𝑥) ↔ (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)))
22	3, 21	raleqbidv 3329	. . . 4 ⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑦 ∈ (Atoms‘𝑘)𝑦(le‘𝑘)𝑥) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)))
23	8, 22	anbi12d 632	. . 3 ⊢ (𝑘 = 𝐾 → (((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑦 ∈ (Atoms‘𝑘)𝑦(le‘𝑘)𝑥)) ↔ (𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))))
24		df-atl 39274	. . 3 ⊢ AtLat = {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑦 ∈ (Atoms‘𝑘)𝑦(le‘𝑘)𝑥))}
25	23, 24	elrab2 3678	. 2 ⊢ (𝐾 ∈ AtLat ↔ (𝐾 ∈ Lat ∧ (𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))))
26		3anass 1094	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) ↔ (𝐾 ∈ Lat ∧ (𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))))
27	25, 26	bitr4i 278	1 ⊢ (𝐾 ∈ AtLat ↔ (𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2931  ∀wral 3050  ∃wrex 3059   class class class wbr 5123  dom cdm 5665  ‘cfv 6541  Basecbs 17230  lecple 17281  glbcglb 18327  0.cp0 18438  Latclat 18446  Atomscatm 39239  AtLatcal 39240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-dm 5675  df-iota 6494  df-fv 6549  df-atl 39274

This theorem is referenced by:  atllat  39276  atl0dm  39278  atlex  39292