meetdm3

Description: The meet of any two elements always exists iff all unordered pairs have GLB (expanded version). (Contributed by Zhi Wang, 25-Sep-2024)

	Ref	Expression
Hypotheses	joindm2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	joindm2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	meetdm2.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
	meetdm2.m	⊢ ∧ = ( meet ‘ 𝐾 )
	meetdm3.l	⊢ ≤ = ( le ‘ 𝐾 )
Assertion	meetdm3	⊢ ( 𝜑 → ( dom ∧ = ( 𝐵 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃! 𝑧 ∈ 𝐵 ( ( 𝑧 ≤ 𝑥 ∧ 𝑧 ≤ 𝑦 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑤 ≤ 𝑥 ∧ 𝑤 ≤ 𝑦 ) → 𝑤 ≤ 𝑧 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		joindm2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		joindm2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
3		meetdm2.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		meetdm2.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		meetdm3.l	⊢ ≤ = ( le ‘ 𝐾 )
6	1 2 3 4	meetdm2	⊢ ( 𝜑 → ( dom ∧ = ( 𝐵 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝐺 ) )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
8		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
9	7 8	prssd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → { 𝑥 , 𝑦 } ⊆ 𝐵 )
10		biid	⊢ ( ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑧 ≤ 𝑣 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑤 ≤ 𝑣 → 𝑤 ≤ 𝑧 ) ) ↔ ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑧 ≤ 𝑣 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑤 ≤ 𝑣 → 𝑤 ≤ 𝑧 ) ) )
11	1 5 3 10 2	glbeldm	⊢ ( 𝜑 → ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑧 ≤ 𝑣 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑤 ≤ 𝑣 → 𝑤 ≤ 𝑧 ) ) ) ) )
12	11	baibd	⊢ ( ( 𝜑 ∧ { 𝑥 , 𝑦 } ⊆ 𝐵 ) → ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ↔ ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑧 ≤ 𝑣 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑤 ≤ 𝑣 → 𝑤 ≤ 𝑧 ) ) ) )
13	9 12	syldan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ↔ ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑧 ≤ 𝑣 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑤 ≤ 𝑣 → 𝑤 ≤ 𝑧 ) ) ) )
14	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐾 ∈ 𝑉 )
15	1 5 4 14 7 8	meetval2lem	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑧 ≤ 𝑣 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑤 ≤ 𝑣 → 𝑤 ≤ 𝑧 ) ) ↔ ( ( 𝑧 ≤ 𝑥 ∧ 𝑧 ≤ 𝑦 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑤 ≤ 𝑥 ∧ 𝑤 ≤ 𝑦 ) → 𝑤 ≤ 𝑧 ) ) ) )
16	15	reubidv	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑧 ≤ 𝑣 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑤 ≤ 𝑣 → 𝑤 ≤ 𝑧 ) ) ↔ ∃! 𝑧 ∈ 𝐵 ( ( 𝑧 ≤ 𝑥 ∧ 𝑧 ≤ 𝑦 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑤 ≤ 𝑥 ∧ 𝑤 ≤ 𝑦 ) → 𝑤 ≤ 𝑧 ) ) ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑧 ≤ 𝑣 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑣 ∈ { 𝑥 , 𝑦 } 𝑤 ≤ 𝑣 → 𝑤 ≤ 𝑧 ) ) ↔ ∃! 𝑧 ∈ 𝐵 ( ( 𝑧 ≤ 𝑥 ∧ 𝑧 ≤ 𝑦 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑤 ≤ 𝑥 ∧ 𝑤 ≤ 𝑦 ) → 𝑤 ≤ 𝑧 ) ) ) )
18	13 17	bitrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ↔ ∃! 𝑧 ∈ 𝐵 ( ( 𝑧 ≤ 𝑥 ∧ 𝑧 ≤ 𝑦 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑤 ≤ 𝑥 ∧ 𝑤 ≤ 𝑦 ) → 𝑤 ≤ 𝑧 ) ) ) )
19	18	2ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃! 𝑧 ∈ 𝐵 ( ( 𝑧 ≤ 𝑥 ∧ 𝑧 ≤ 𝑦 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑤 ≤ 𝑥 ∧ 𝑤 ≤ 𝑦 ) → 𝑤 ≤ 𝑧 ) ) ) )
20	6 19	bitrd	⊢ ( 𝜑 → ( dom ∧ = ( 𝐵 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃! 𝑧 ∈ 𝐵 ( ( 𝑧 ≤ 𝑥 ∧ 𝑧 ≤ 𝑦 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ( 𝑤 ≤ 𝑥 ∧ 𝑤 ≤ 𝑦 ) → 𝑤 ≤ 𝑧 ) ) ) )

Metamath Proof Explorer

Theorem meetdm3

Proof