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 𝐺 ↔ ( 𝑆𝐵 ∧ ∃! 𝑥𝐵 𝜓 ) ) )