Metamath Proof Explorer

Theorem glbeldm

Description: Member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018)

Ref Expression
Hypotheses glbeldm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
glbeldm.l ⊢ ≤ = ( le ‘ 𝐾 )
glbeldm.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
glbeldm.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
glbeldm.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
Assertion glbeldm ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 glbeldm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 glbeldm.l ⊢ ≤ = ( le ‘ 𝐾 )
3 glbeldm.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
4 glbeldm.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
5 glbeldm.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
6 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
7 1 2 3 6 5 glbdm ⊢ ( 𝜑 → dom 𝐺 = { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } )
8 7 eleq2d ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ) )
9 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) )
10 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 ) )
11 10 imbi1d ⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
12 11 ralbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
13 9 12 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
14 13 reubidv ⊢ ( 𝑠 = 𝑆 → ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
15 4 reubii ⊢ ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
16 14 15 bitr4di ⊢ ( 𝑠 = 𝑆 → ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
17 16 elrab ⊢ ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
18 1 fvexi ⊢ 𝐵 ∈ V
19 18 elpw2 ⊢ ( 𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵 )
20 19 anbi1i ⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
21 17 20 bitri ⊢ ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
22 8 21 bitrdi ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) )