Theorem meetdmss

Description: Subset property of domain of meet. (Contributed by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	meetdmss.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	meetdmss.j	⊢ ∧ = ( meet ‘ 𝐾 )
	meetdmss.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
Assertion	meetdmss	⊢ ( 𝜑 → dom ∧ ⊆ ( 𝐵 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		meetdmss.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		meetdmss.j	⊢ ∧ = ( meet ‘ 𝐾 )
3		meetdmss.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
4		relopabv	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) }
5		eqid	⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
6	5 2	meetdm	⊢ ( 𝐾 ∈ 𝑉 → dom ∧ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) } )
7	3 6	syl	⊢ ( 𝜑 → dom ∧ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) } )
8	7	releqd	⊢ ( 𝜑 → ( Rel dom ∧ ↔ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) } ) )
9	4 8	mpbiri	⊢ ( 𝜑 → Rel dom ∧ )
10		vex	⊢ 𝑥 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝑥 ∈ V )
12		vex	⊢ 𝑦 ∈ V
13	12	a1i	⊢ ( 𝜑 → 𝑦 ∈ V )
14	5 2 3 11 13	meetdef	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∧ ↔ { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) ) )
15		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
16	3	adantr	⊢ ( ( 𝜑 ∧ { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) ) → 𝐾 ∈ 𝑉 )
17		simpr	⊢ ( ( 𝜑 ∧ { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) ) → { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) )
18	1 15 5 16 17	glbelss	⊢ ( ( 𝜑 ∧ { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) ) → { 𝑥 , 𝑦 } ⊆ 𝐵 )
19	18	ex	⊢ ( 𝜑 → ( { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) → { 𝑥 , 𝑦 } ⊆ 𝐵 ) )
20	10 12	prss	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 )
21		opelxpi	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) )
22	20 21	sylbir	⊢ ( { 𝑥 , 𝑦 } ⊆ 𝐵 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) )
23	19 22	syl6	⊢ ( 𝜑 → ( { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ) )
24	14 23	sylbid	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ∧ → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ) )
25	9 24	relssdv	⊢ ( 𝜑 → dom ∧ ⊆ ( 𝐵 × 𝐵 ) )