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 bitrid ⊢ ( ( 𝐾 ∈ 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 ∧ 𝑆 ⊆ 𝐵 ) → ∃* 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )