This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lubval

Description: Value of the least upper bound function of a poset. Out-of-domain arguments (those not satisfying S e. dom U ) are allowed for convenience, evaluating to the empty set. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

Ref Expression
Hypotheses lubval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lubval.l ⊢ ≤ = ( le ‘ 𝐾 )
lubval.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
lubval.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
lubval.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
lubval.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion lubval ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )

Proof

Step Hyp Ref Expression
1 lubval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lubval.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lubval.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 lubval.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
5 lubval.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
6 lubval.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
7 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
8 5 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → 𝐾 ∈ 𝑉 )
9 1 2 3 7 8 lubfval ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → 𝑈 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ) )
10 9 fveq1d ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → ( 𝑈 ‘ 𝑆 ) = ( ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ) ‘ 𝑆 ) )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → 𝑆 ∈ dom 𝑈 )
12 1 2 3 4 8 11 lubeu ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → ∃! 𝑥 ∈ 𝐵 𝜓 )
13 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )
14 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ) )
15 14 imbi1d ⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
16 15 ralbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
17 13 16 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) )
18 17 4 bitr4di ⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ 𝜓 ) )
19 18 reubidv ⊢ ( 𝑠 = 𝑆 → ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
20 11 12 19 elabd ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → 𝑆 ∈ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } )
21 20 fvresd ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → ( ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ) ‘ 𝑆 ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ‘ 𝑆 ) )
22 6 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → 𝑆 ⊆ 𝐵 )
23 1 fvexi ⊢ 𝐵 ∈ V
24 23 elpw2 ⊢ ( 𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵 )
25 22 24 sylibr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → 𝑆 ∈ 𝒫 𝐵 )
26 18 riotabidv ⊢ ( 𝑠 = 𝑆 → ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
27 eqid ⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) )
28 riotaex ⊢ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ∈ V
29 26 27 28 fvmpt ⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
30 25 29 syl ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
31 10 21 30 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝑈 ) → ( 𝑈 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
32 ndmfv ⊢ ( ¬ 𝑆 ∈ dom 𝑈 → ( 𝑈 ‘ 𝑆 ) = ∅ )
33 32 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ dom 𝑈 ) → ( 𝑈 ‘ 𝑆 ) = ∅ )
34 1 2 3 4 5 lubeldm ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) )
35 34 biimprd ⊢ ( 𝜑 → ( ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) → 𝑆 ∈ dom 𝑈 ) )
36 6 35 mpand ⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 → 𝑆 ∈ dom 𝑈 ) )
37 36 con3dimp ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ dom 𝑈 ) → ¬ ∃! 𝑥 ∈ 𝐵 𝜓 )
38 riotaund ⊢ ( ¬ ∃! 𝑥 ∈ 𝐵 𝜓 → ( ℩ 𝑥 ∈ 𝐵 𝜓 ) = ∅ )
39 37 38 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ dom 𝑈 ) → ( ℩ 𝑥 ∈ 𝐵 𝜓 ) = ∅ )
40 33 39 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ dom 𝑈 ) → ( 𝑈 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
41 31 40 pm2.61dan ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )