Metamath Proof Explorer

Theorem lubfval

Description: Value of the least upper bound function of a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 6-Sep-2018)

Ref Expression
Hypotheses lubfval.b ⊢ B = Base K
lubfval.l ⊢ ≤ ˙ = ≤ K
lubfval.u ⊢ U = lub ⁡ K
lubfval.p ⊢ ψ ↔ ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
lubfval.k ⊢ φ → K ∈ V
Assertion lubfval ⊢ φ → U = s ∈ 𝒫 B ⟼ ι x ∈ B | ψ ↾ s | ∃! x ∈ B ψ

Proof

Step Hyp Ref Expression
1 lubfval.b ⊢ B = Base K
2 lubfval.l ⊢ ≤ ˙ = ≤ K
3 lubfval.u ⊢ U = lub ⁡ K
4 lubfval.p ⊢ ψ ↔ ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
5 lubfval.k ⊢ φ → K ∈ V
6 elex ⊢ K ∈ V → K ∈ V
7 fveq2 ⊢ p = K → Base p = Base K
8 7 1 eqtr4di ⊢ p = K → Base p = B
9 8 pweqd ⊢ p = K → 𝒫 Base p = 𝒫 B
10 fveq2 ⊢ p = K → ≤ p = ≤ K
11 10 2 eqtr4di ⊢ p = K → ≤ p = ≤ ˙
12 11 breqd ⊢ p = K → y ≤ p x ↔ y ≤ ˙ x
13 12 ralbidv ⊢ p = K → ∀ y ∈ s y ≤ p x ↔ ∀ y ∈ s y ≤ ˙ x
14 11 breqd ⊢ p = K → y ≤ p z ↔ y ≤ ˙ z
15 14 ralbidv ⊢ p = K → ∀ y ∈ s y ≤ p z ↔ ∀ y ∈ s y ≤ ˙ z
16 11 breqd ⊢ p = K → x ≤ p z ↔ x ≤ ˙ z
17 15 16 imbi12d ⊢ p = K → ∀ y ∈ s y ≤ p z → x ≤ p z ↔ ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
18 8 17 raleqbidv ⊢ p = K → ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z ↔ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
19 13 18 anbi12d ⊢ p = K → ∀ y ∈ s y ≤ p x ∧ ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z ↔ ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
20 8 19 riotaeqbidv ⊢ p = K → ι x ∈ Base p | ∀ y ∈ s y ≤ p x ∧ ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z = ι x ∈ B | ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
21 9 20 mpteq12dv ⊢ p = K → s ∈ 𝒫 Base p ⟼ ι x ∈ Base p | ∀ y ∈ s y ≤ p x ∧ ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z = s ∈ 𝒫 B ⟼ ι x ∈ B | ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
22 19 reubidv ⊢ p = K → ∃! x ∈ Base p ∀ y ∈ s y ≤ p x ∧ ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z ↔ ∃! x ∈ Base p ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
23 reueq1 ⊢ Base p = B → ∃! x ∈ Base p ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z ↔ ∃! x ∈ B ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
24 8 23 syl ⊢ p = K → ∃! x ∈ Base p ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z ↔ ∃! x ∈ B ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
25 22 24 bitrd ⊢ p = K → ∃! x ∈ Base p ∀ y ∈ s y ≤ p x ∧ ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z ↔ ∃! x ∈ B ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
26 25 abbidv ⊢ p = K → s | ∃! x ∈ Base p ∀ y ∈ s y ≤ p x ∧ ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z = s | ∃! x ∈ B ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
27 21 26 reseq12d ⊢ p = K → s ∈ 𝒫 Base p ⟼ ι x ∈ Base p | ∀ y ∈ s y ≤ p x ∧ ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z ↾ s | ∃! x ∈ Base p ∀ y ∈ s y ≤ p x ∧ ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z = s ∈ 𝒫 B ⟼ ι x ∈ B | ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z ↾ s | ∃! x ∈ B ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
28 df-lub ⊢ lub = p ∈ V ⟼ s ∈ 𝒫 Base p ⟼ ι x ∈ Base p | ∀ y ∈ s y ≤ p x ∧ ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z ↾ s | ∃! x ∈ Base p ∀ y ∈ s y ≤ p x ∧ ∀ z ∈ Base p ∀ y ∈ s y ≤ p z → x ≤ p z
29 1 fvexi ⊢ B ∈ V
30 29 pwex ⊢ 𝒫 B ∈ V
31 30 mptex ⊢ s ∈ 𝒫 B ⟼ ι x ∈ B | ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z ∈ V
32 31 resex ⊢ s ∈ 𝒫 B ⟼ ι x ∈ B | ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z ↾ s | ∃! x ∈ B ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z ∈ V
33 27 28 32 fvmpt ⊢ K ∈ V → lub ⁡ K = s ∈ 𝒫 B ⟼ ι x ∈ B | ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z ↾ s | ∃! x ∈ B ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
34 4 a1i ⊢ x ∈ B → ψ ↔ ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
35 34 riotabiia ⊢ ι x ∈ B | ψ = ι x ∈ B | ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
36 35 mpteq2i ⊢ s ∈ 𝒫 B ⟼ ι x ∈ B | ψ = s ∈ 𝒫 B ⟼ ι x ∈ B | ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
37 4 reubii ⊢ ∃! x ∈ B ψ ↔ ∃! x ∈ B ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
38 37 abbii ⊢ s | ∃! x ∈ B ψ = s | ∃! x ∈ B ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
39 36 38 reseq12i ⊢ s ∈ 𝒫 B ⟼ ι x ∈ B | ψ ↾ s | ∃! x ∈ B ψ = s ∈ 𝒫 B ⟼ ι x ∈ B | ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z ↾ s | ∃! x ∈ B ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
40 33 3 39 3eqtr4g ⊢ K ∈ V → U = s ∈ 𝒫 B ⟼ ι x ∈ B | ψ ↾ s | ∃! x ∈ B ψ
41 5 6 40 3syl ⊢ φ → U = s ∈ 𝒫 B ⟼ ι x ∈ B | ψ ↾ s | ∃! x ∈ B ψ