Metamath Proof Explorer

Theorem glbeldm2d

Description: Member of the domain of the greatest lower bound function of a poset. (Contributed by Zhi Wang, 29-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 lubeldm2d.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 lubeldm2d.l ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐾 ) )
3 glbeldm2d.g ⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐾 ) )
4 glbeldm2d.p ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
5 glbeldm2d.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
9 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
10 6 7 8 9 5 glbeldm2 ⊢ ( 𝜑 → ( 𝑆 ∈ dom ( glb ‘ 𝐾 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐾 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) )
11 3 dmeqd ⊢ ( 𝜑 → dom 𝐺 = dom ( glb ‘ 𝐾 ) )
12 11 eleq2d ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ 𝑆 ∈ dom ( glb ‘ 𝐾 ) ) )
13 1 sseq2d ⊢ ( 𝜑 → ( 𝑆 ⊆ 𝐵 ↔ 𝑆 ⊆ ( Base ‘ 𝐾 ) ) )
14 2 breqd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) )
15 14 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ) )
16 2 breqd ⊢ ( 𝜑 → ( 𝑧 ≤ 𝑦 ↔ 𝑧 ( le ‘ 𝐾 ) 𝑦 ) )
17 16 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 ) )
18 2 breqd ⊢ ( 𝜑 → ( 𝑧 ≤ 𝑥 ↔ 𝑧 ( le ‘ 𝐾 ) 𝑥 ) )
19 17 18 imbi12d ⊢ ( 𝜑 → ( ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
20 1 19 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
21 15 20 anbi12d ⊢ ( 𝜑 → ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) )
23 4 22 bitrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) )
24 23 pm5.32da ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) )
25 1 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝐾 ) ) )
26 25 anbi1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) )
27 24 26 bitrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) )
28 27 rexbidv2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 𝜓 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) )
29 13 28 anbi12d ⊢ ( 𝜑 → ( ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐾 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) )
30 10 12 29 3bitr4d ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) )