# Metamath Proof Explorer

## Theorem posglbmo

Description: Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018)

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

### Proof

Step Hyp Ref Expression
1 poslubmo.l = ( le ‘ 𝐾 )
2 poslubmo.b 𝐵 = ( Base ‘ 𝐾 )
3 simprrl ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆𝐵 ) ∧ ( 𝑥𝐵𝑤𝐵 ) ) ∧ ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ∧ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) ) → ∀ 𝑦𝑆 𝑤 𝑦 )
4 breq1 ( 𝑧 = 𝑤 → ( 𝑧 𝑦𝑤 𝑦 ) )
5 4 ralbidv ( 𝑧 = 𝑤 → ( ∀ 𝑦𝑆 𝑧 𝑦 ↔ ∀ 𝑦𝑆 𝑤 𝑦 ) )
6 breq1 ( 𝑧 = 𝑤 → ( 𝑧 𝑥𝑤 𝑥 ) )
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 breq1 ( 𝑧 = 𝑥 → ( 𝑧 𝑦𝑥 𝑦 ) )
14 13 ralbidv ( 𝑧 = 𝑥 → ( ∀ 𝑦𝑆 𝑧 𝑦 ↔ ∀ 𝑦𝑆 𝑥 𝑦 ) )
15 breq1 ( 𝑧 = 𝑥 → ( 𝑧 𝑤𝑥 𝑤 ) )
16 14 15 imbi12d ( 𝑧 = 𝑥 → ( ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ↔ ( ∀ 𝑦𝑆 𝑥 𝑦𝑥 𝑤 ) ) )
17 simprrr ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆𝐵 ) ∧ ( 𝑥𝐵𝑤𝐵 ) ) ∧ ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ∧ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) ) → ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) )
18 simplrl ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆𝐵 ) ∧ ( 𝑥𝐵𝑤𝐵 ) ) ∧ ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ∧ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) ) → 𝑥𝐵 )
19 16 17 18 rspcdva ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆𝐵 ) ∧ ( 𝑥𝐵𝑤𝐵 ) ) ∧ ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ∧ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) ) → ( ∀ 𝑦𝑆 𝑥 𝑦𝑥 𝑤 ) )
20 12 19 mpd ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆𝐵 ) ∧ ( 𝑥𝐵𝑤𝐵 ) ) ∧ ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ∧ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) ) → 𝑥 𝑤 )
21 ancom ( ( 𝑤 𝑥𝑥 𝑤 ) ↔ ( 𝑥 𝑤𝑤 𝑥 ) )
22 2 1 posasymb ( ( 𝐾 ∈ Poset ∧ 𝑥𝐵𝑤𝐵 ) → ( ( 𝑥 𝑤𝑤 𝑥 ) ↔ 𝑥 = 𝑤 ) )
23 21 22 syl5bb ( ( 𝐾 ∈ Poset ∧ 𝑥𝐵𝑤𝐵 ) → ( ( 𝑤 𝑥𝑥 𝑤 ) ↔ 𝑥 = 𝑤 ) )
24 23 3expb ( ( 𝐾 ∈ Poset ∧ ( 𝑥𝐵𝑤𝐵 ) ) → ( ( 𝑤 𝑥𝑥 𝑤 ) ↔ 𝑥 = 𝑤 ) )
25 24 ad4ant13 ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆𝐵 ) ∧ ( 𝑥𝐵𝑤𝐵 ) ) ∧ ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ∧ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) ) → ( ( 𝑤 𝑥𝑥 𝑤 ) ↔ 𝑥 = 𝑤 ) )
26 11 20 25 mpbi2and ( ( ( ( 𝐾 ∈ Poset ∧ 𝑆𝐵 ) ∧ ( 𝑥𝐵𝑤𝐵 ) ) ∧ ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ∧ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) ) → 𝑥 = 𝑤 )
27 26 ex ( ( ( 𝐾 ∈ Poset ∧ 𝑆𝐵 ) ∧ ( 𝑥𝐵𝑤𝐵 ) ) → ( ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ∧ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) → 𝑥 = 𝑤 ) )
28 27 ralrimivva ( ( 𝐾 ∈ Poset ∧ 𝑆𝐵 ) → ∀ 𝑥𝐵𝑤𝐵 ( ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ∧ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) → 𝑥 = 𝑤 ) )
29 breq1 ( 𝑥 = 𝑤 → ( 𝑥 𝑦𝑤 𝑦 ) )
30 29 ralbidv ( 𝑥 = 𝑤 → ( ∀ 𝑦𝑆 𝑥 𝑦 ↔ ∀ 𝑦𝑆 𝑤 𝑦 ) )
31 breq2 ( 𝑥 = 𝑤 → ( 𝑧 𝑥𝑧 𝑤 ) )
32 31 imbi2d ( 𝑥 = 𝑤 → ( ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ↔ ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) )
33 32 ralbidv ( 𝑥 = 𝑤 → ( ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ↔ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) )
34 30 33 anbi12d ( 𝑥 = 𝑤 → ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ↔ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) )
35 34 rmo4 ( ∃* 𝑥𝐵 ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ↔ ∀ 𝑥𝐵𝑤𝐵 ( ( ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) ∧ ( ∀ 𝑦𝑆 𝑤 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑤 ) ) ) → 𝑥 = 𝑤 ) )
36 28 35 sylibr ( ( 𝐾 ∈ Poset ∧ 𝑆𝐵 ) → ∃* 𝑥𝐵 ( ∀ 𝑦𝑆 𝑥 𝑦 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑧 𝑦𝑧 𝑥 ) ) )