Metamath Proof Explorer

Theorem lubeldm2d

Description: Member of the domain of the least upper bound function of a poset. (Contributed by Zhi Wang, 28-Sep-2024)

Ref Expression
Hypotheses lubeldm2d.b ⊢φ→B=BaseK
lubeldm2d.l ⊢φ→≤˙=≤K
lubeldm2d.u ⊢φ→U=lub⁡K
lubeldm2d.p ⊢φ∧x∈B→ψ↔∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z
lubeldm2d.k ⊢φ→K∈Poset
Assertion lubeldm2d ⊢φ→S∈dom⁡U↔S⊆B∧∃x∈Bψ

Proof

Step Hyp Ref Expression
1 lubeldm2d.b ⊢φ→B=BaseK
2 lubeldm2d.l ⊢φ→≤˙=≤K
3 lubeldm2d.u ⊢φ→U=lub⁡K
4 lubeldm2d.p ⊢φ∧x∈B→ψ↔∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z
5 lubeldm2d.k ⊢φ→K∈Poset
6 eqid ⊢BaseK=BaseK
7 eqid ⊢≤K=≤K
8 eqid ⊢lub⁡K=lub⁡K
9 biid ⊢∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz↔∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
10 6 7 8 9 5 lubeldm2 ⊢φ→S∈dom⁡lub⁡K↔S⊆BaseK∧∃x∈BaseK∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
11 3 dmeqd ⊢φ→dom⁡U=dom⁡lub⁡K
12 11 eleq2d ⊢φ→S∈dom⁡U↔S∈dom⁡lub⁡K
13 1 sseq2d ⊢φ→S⊆B↔S⊆BaseK
14 2 breqd ⊢φ→y≤˙x↔y≤Kx
15 14 ralbidv ⊢φ→∀y∈Sy≤˙x↔∀y∈Sy≤Kx
16 2 breqd ⊢φ→y≤˙z↔y≤Kz
17 16 ralbidv ⊢φ→∀y∈Sy≤˙z↔∀y∈Sy≤Kz
18 2 breqd ⊢φ→x≤˙z↔x≤Kz
19 17 18 imbi12d ⊢φ→∀y∈Sy≤˙z→x≤˙z↔∀y∈Sy≤Kz→x≤Kz
20 1 19 raleqbidv ⊢φ→∀z∈B∀y∈Sy≤˙z→x≤˙z↔∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
21 15 20 anbi12d ⊢φ→∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z↔∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
22 21 adantr ⊢φ∧x∈B→∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z↔∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
23 4 22 bitrd ⊢φ∧x∈B→ψ↔∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
24 23 pm5.32da ⊢φ→x∈B∧ψ↔x∈B∧∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
25 1 eleq2d ⊢φ→x∈B↔x∈BaseK
26 25 anbi1d ⊢φ→x∈B∧∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz↔x∈BaseK∧∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
27 24 26 bitrd ⊢φ→x∈B∧ψ↔x∈BaseK∧∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
28 27 rexbidv2 ⊢φ→∃x∈Bψ↔∃x∈BaseK∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
29 13 28 anbi12d ⊢φ→S⊆B∧∃x∈Bψ↔S⊆BaseK∧∃x∈BaseK∀y∈Sy≤Kx∧∀z∈BaseK∀y∈Sy≤Kz→x≤Kz
30 10 12 29 3bitr4d ⊢φ→S∈dom⁡U↔S⊆B∧∃x∈Bψ