Metamath Proof Explorer


Theorem joindmss

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

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

Proof

Step Hyp Ref Expression
1 joindmss.b
 |-  B = ( Base ` K )
2 joindmss.j
 |-  .\/ = ( join ` K )
3 joindmss.k
 |-  ( ph -> K e. V )
4 relopabv
 |-  Rel { <. x , y >. | { x , y } e. dom ( lub ` K ) }
5 eqid
 |-  ( lub ` K ) = ( lub ` K )
6 5 2 joindm
 |-  ( K e. V -> dom .\/ = { <. x , y >. | { x , y } e. dom ( lub ` K ) } )
7 3 6 syl
 |-  ( ph -> dom .\/ = { <. x , y >. | { x , y } e. dom ( lub ` K ) } )
8 7 releqd
 |-  ( ph -> ( Rel dom .\/ <-> Rel { <. x , y >. | { x , y } e. dom ( lub ` 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 joindef
 |-  ( ph -> ( <. x , y >. e. dom .\/ <-> { x , y } e. dom ( lub ` K ) ) )
15 eqid
 |-  ( le ` K ) = ( le ` K )
16 3 adantr
 |-  ( ( ph /\ { x , y } e. dom ( lub ` K ) ) -> K e. V )
17 simpr
 |-  ( ( ph /\ { x , y } e. dom ( lub ` K ) ) -> { x , y } e. dom ( lub ` K ) )
18 1 15 5 16 17 lubelss
 |-  ( ( ph /\ { x , y } e. dom ( lub ` K ) ) -> { x , y } C_ B )
19 18 ex
 |-  ( ph -> ( { x , y } e. dom ( lub ` 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 ( lub ` 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 ) )