Theorem meetdm2

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

	Ref	Expression
Hypotheses	joindm2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	joindm2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	meetdm2.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
	meetdm2.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	meetdm2	⊢ ( 𝜑 → ( dom ∧ = ( 𝐵 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		joindm2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		joindm2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
3		meetdm2.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		meetdm2.m	⊢ ∧ = ( meet ‘ 𝐾 )
5	1 4 2	meetdmss	⊢ ( 𝜑 → dom ∧ ⊆ ( 𝐵 × 𝐵 ) )
6		eqss	⊢ ( dom ∧ = ( 𝐵 × 𝐵 ) ↔ ( dom ∧ ⊆ ( 𝐵 × 𝐵 ) ∧ ( 𝐵 × 𝐵 ) ⊆ dom ∧ ) )
7	6	baib	⊢ ( dom ∧ ⊆ ( 𝐵 × 𝐵 ) → ( dom ∧ = ( 𝐵 × 𝐵 ) ↔ ( 𝐵 × 𝐵 ) ⊆ dom ∧ ) )
8	5 7	syl	⊢ ( 𝜑 → ( dom ∧ = ( 𝐵 × 𝐵 ) ↔ ( 𝐵 × 𝐵 ) ⊆ dom ∧ ) )
9		relxp	⊢ Rel ( 𝐵 × 𝐵 )
10		ssrel	⊢ ( Rel ( 𝐵 × 𝐵 ) → ( ( 𝐵 × 𝐵 ) ⊆ dom ∧ ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∧ ) ) )
11	9 10	mp1i	⊢ ( 𝜑 → ( ( 𝐵 × 𝐵 ) ⊆ dom ∧ ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∧ ) ) )
12		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
13	12	a1i	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
14		vex	⊢ 𝑥 ∈ V
15	14	a1i	⊢ ( 𝜑 → 𝑥 ∈ V )
16		vex	⊢ 𝑦 ∈ V
17	16	a1i	⊢ ( 𝜑 → 𝑦 ∈ V )
18	3 4 2 15 17	meetdef	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∧ ↔ { 𝑥 , 𝑦 } ∈ dom 𝐺 ) )
19	13 18	imbi12d	⊢ ( 𝜑 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∧ ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , 𝑦 } ∈ dom 𝐺 ) ) )
20	19	2albidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∧ ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , 𝑦 } ∈ dom 𝐺 ) ) )
21		r2al	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝐺 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → { 𝑥 , 𝑦 } ∈ dom 𝐺 ) )
22	20 21	bitr4di	⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∧ ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝐺 ) )
23	8 11 22	3bitrd	⊢ ( 𝜑 → ( dom ∧ = ( 𝐵 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 { 𝑥 , 𝑦 } ∈ dom 𝐺 ) )