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