# 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 ∧ 𝑆𝐵 ) → ∃* 𝑥𝐵 ( ∀ 𝑦𝑆 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ) )