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 ) )