Metamath Proof Explorer

Theorem meetdmss

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

Ref Expression
Hypotheses meetdmss.b 
|- B = ( Base ` K )
meetdmss.j 
|- ./\ = ( meet ` K )
meetdmss.k 
|- ( ph -> K e. V )
Assertion meetdmss 
|- ( ph -> dom ./\ C_ ( B X. B ) )

Proof

Step Hyp Ref Expression
1 meetdmss.b 
 |-  B = ( Base ` K )
2 meetdmss.j 
 |-  ./\ = ( meet ` K )
3 meetdmss.k 
 |-  ( ph -> K e. V )
4 relopabv 
 |-  Rel { <. x , y >. | { x , y } e. dom ( glb ` K ) }
5 eqid 
 |-  ( glb ` K ) = ( glb ` K )
6 5 2 meetdm 
 |-  ( K e. V -> dom ./\ = { <. x , y >. | { x , y } e. dom ( glb ` K ) } )
7 3 6 syl 
 |-  ( ph -> dom ./\ = { <. x , y >. | { x , y } e. dom ( glb ` K ) } )
8 7 releqd 
 |-  ( ph -> ( Rel dom ./\ <-> Rel { <. x , y >. | { x , y } e. dom ( glb ` K ) } ) )
9 4 8 mpbiri 
 |-  ( ph -> Rel dom ./\ )
10 vex 
 |-  x e. _V
11 10 a1i 
 |-  ( ph -> x e. _V )
12 vex 
 |-  y e. _V
13 12 a1i 
 |-  ( ph -> y e. _V )
14 5 2 3 11 13 meetdef 
 |-  ( ph -> ( <. x , y >. e. dom ./\ <-> { x , y } e. dom ( glb ` K ) ) )
15 eqid 
 |-  ( le ` K ) = ( le ` K )
16 3 adantr 
 |-  ( ( ph /\ { x , y } e. dom ( glb ` K ) ) -> K e. V )
17 simpr 
 |-  ( ( ph /\ { x , y } e. dom ( glb ` K ) ) -> { x , y } e. dom ( glb ` K ) )
18 1 15 5 16 17 glbelss 
 |-  ( ( ph /\ { x , y } e. dom ( glb ` K ) ) -> { x , y } C_ B )
19 18 ex 
 |-  ( ph -> ( { x , y } e. dom ( glb ` K ) -> { x , y } C_ B ) )
20 10 12 prss 
 |-  ( ( x e. B /\ y e. B ) <-> { x , y } C_ B )
21 opelxpi 
 |-  ( ( x e. B /\ y e. B ) -> <. x , y >. e. ( B X. B ) )
22 20 21 sylbir 
 |-  ( { x , y } C_ B -> <. x , y >. e. ( B X. B ) )
23 19 22 syl6 
 |-  ( ph -> ( { x , y } e. dom ( glb ` K ) -> <. x , y >. e. ( B X. B ) ) )
24 14 23 sylbid 
 |-  ( ph -> ( <. x , y >. e. dom ./\ -> <. x , y >. e. ( B X. B ) ) )
25 9 24 relssdv 
 |-  ( ph -> dom ./\ C_ ( B X. B ) )