Metamath Proof Explorer

Theorem poslubmo

Description: Least upper bounds in a poset are unique if they exist. (Contributed by Stefan O'Rear, 31-Jan-2015) (Revised by NM, 16-Jun-2017)

Ref Expression
Hypotheses poslubmo.l ⊢ ≤ = ( le ‘ 𝐾 )
poslubmo.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
Assertion poslubmo ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) → ∃* 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 poslubmo.l ⊢ ≤ = ( le ‘ 𝐾 )
2 poslubmo.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
3 simprrl ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 )
4 breq2 ⊢ ( 𝑧 = 𝑤 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ≤ 𝑤 ) )
5 4 ralbidv ⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ) )
6 breq2 ⊢ ( 𝑧 = 𝑤 → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ≤ 𝑤 ) )
7 5 6 imbi12d ⊢ ( 𝑧 = 𝑤 → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) )
8 simprlr ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) )
9 simplrr ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → 𝑤 ∈ 𝐵 )
10 7 8 9 rspcdva ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) )
11 3 10 mpd ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → 𝑥 ≤ 𝑤 )
12 simprll ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 )
13 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ≤ 𝑥 ) )
14 13 ralbidv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )
15 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑤 ≤ 𝑧 ↔ 𝑤 ≤ 𝑥 ) )
16 14 15 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 → 𝑤 ≤ 𝑥 ) ) )
17 simprrr ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) )
18 simplrl ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → 𝑥 ∈ 𝐵 )
19 16 17 18 rspcdva ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 → 𝑤 ≤ 𝑥 ) )
20 12 19 mpd ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → 𝑤 ≤ 𝑥 )
21 2 1 posasymb ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑥 ) ↔ 𝑥 = 𝑤 ) )
22 21 3expb ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑥 ) ↔ 𝑥 = 𝑤 ) )
23 22 ad4ant13 ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → ( ( 𝑥 ≤ 𝑤 ∧ 𝑤 ≤ 𝑥 ) ↔ 𝑥 = 𝑤 ) )
24 11 20 23 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) ) → 𝑥 = 𝑤 )
25 24 ex ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) → 𝑥 = 𝑤 ) )
26 25 ralrimivva ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) → 𝑥 = 𝑤 ) )
27 breq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑤 ) )
28 27 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ) )
29 breq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ≤ 𝑧 ↔ 𝑤 ≤ 𝑧 ) )
30 29 imbi2d ⊢ ( 𝑥 = 𝑤 → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) )
31 30 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) )
32 28 31 anbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) )
33 32 rmo4 ⊢ ( ∃* 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑤 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑤 ≤ 𝑧 ) ) ) → 𝑥 = 𝑤 ) )
34 26 33 sylibr ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) → ∃* 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )