Theorem glbeldm2 49615

Description: Member of the domain of the greatest lower bound function of a poset. (Contributed by Zhi Wang, 26-Sep-2024.)

Hypotheses

Ref	Expression
lubeldm2.b	⊢ 𝐵 = (Base‘𝐾)
lubeldm2.l	⊢ ≤ = (le‘𝐾)
glbeldm2.g	⊢ 𝐺 = (glb‘𝐾)
glbeldm2.p	⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))
glbeldm2.k	⊢ (𝜑 → 𝐾 ∈ Poset)

Assertion

Ref	Expression
glbeldm2	⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓)))

Distinct variable groups:   𝑥, ≤ ,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧   𝑥,𝐾,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝜓(𝑥,𝑦,𝑧)   𝐺(𝑥,𝑦,𝑧)

Proof of Theorem glbeldm2

Step	Hyp	Ref	Expression
1		lubeldm2.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
2		lubeldm2.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
3		glbeldm2.g	. . . . 5 ⊢ 𝐺 = (glb‘𝐾)
4		glbeldm2.p	. . . . 5 ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))
5		glbeldm2.k	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Poset)
6	1, 2, 3, 4, 5	glbeldm 18416	. . . 4 ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ (𝑆 ⊆ 𝐵 ∧ ∃!𝑥 ∈ 𝐵 𝜓)))
7	6	biimpa 481	. . 3 ⊢ ((𝜑 ∧ 𝑆 ∈ dom 𝐺) → (𝑆 ⊆ 𝐵 ∧ ∃!𝑥 ∈ 𝐵 𝜓))
8		reurex 3380	. . . 4 ⊢ (∃!𝑥 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐵 𝜓)
9	8	anim2i 628	. . 3 ⊢ ((𝑆 ⊆ 𝐵 ∧ ∃!𝑥 ∈ 𝐵 𝜓) → (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓))
10	7, 9	syl 18	. 2 ⊢ ((𝜑 ∧ 𝑆 ∈ dom 𝐺) → (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓))
11		simpl 487	. . 3 ⊢ ((𝜑 ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓)) → 𝜑)
12		simprl 782	. . 3 ⊢ ((𝜑 ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓)) → 𝑆 ⊆ 𝐵)
13	2, 1	posglbmo 18462	. . . . . . . 8 ⊢ ((𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵) → ∃*𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))
14	5, 13	sylan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 ⊆ 𝐵) → ∃*𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))
15	4	rmobii 3384	. . . . . . 7 ⊢ (∃*𝑥 ∈ 𝐵 𝜓 ↔ ∃*𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))
16	14, 15	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ 𝑆 ⊆ 𝐵) → ∃*𝑥 ∈ 𝐵 𝜓)
17	16	anim1ci 627	. . . . 5 ⊢ (((𝜑 ∧ 𝑆 ⊆ 𝐵) ∧ ∃𝑥 ∈ 𝐵 𝜓) → (∃𝑥 ∈ 𝐵 𝜓 ∧ ∃*𝑥 ∈ 𝐵 𝜓))
18		reu5 3378	. . . . 5 ⊢ (∃!𝑥 ∈ 𝐵 𝜓 ↔ (∃𝑥 ∈ 𝐵 𝜓 ∧ ∃*𝑥 ∈ 𝐵 𝜓))
19	17, 18	sylibr 237	. . . 4 ⊢ (((𝜑 ∧ 𝑆 ⊆ 𝐵) ∧ ∃𝑥 ∈ 𝐵 𝜓) → ∃!𝑥 ∈ 𝐵 𝜓)
20	19	anasss 471	. . 3 ⊢ ((𝜑 ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐵 𝜓)
21	6	biimpar 482	. . 3 ⊢ ((𝜑 ∧ (𝑆 ⊆ 𝐵 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → 𝑆 ∈ dom 𝐺)
22	11, 12, 20, 21	syl12anc 849	. 2 ⊢ ((𝜑 ∧ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓)) → 𝑆 ∈ dom 𝐺)
23	10, 22	impbida 812	1 ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  ∃!wreu 3374  ∃*wrmo 3375   ⊆ wss 3913   class class class wbr 5110  dom cdm 5659  ‘cfv 6534  Basecbs 17265  lecple 17313  Posetcpo 18359  glbcglb 18362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5239  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7365  df-proset 18346  df-poset 18365  df-glb 18397

This theorem is referenced by:  glbeldm2d  49617  glbsscl  49619