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 φ K V
Assertion joindmss φ dom ˙ B × B

Proof

Step Hyp Ref Expression
1 joindmss.b B = Base K
2 joindmss.j ˙ = join K
3 joindmss.k φ K V
4 relopabv Rel x y | x y dom lub K
5 eqid lub K = lub K
6 5 2 joindm K V dom ˙ = x y | x y dom lub K
7 3 6 syl φ dom ˙ = x y | x y dom lub K
8 7 releqd φ Rel dom ˙ Rel x y | x y dom lub K
9 4 8 mpbiri φ Rel dom ˙
10 vex x V
11 10 a1i φ x V
12 vex y V
13 12 a1i φ y V
14 5 2 3 11 13 joindef φ x y dom ˙ x y dom lub K
15 eqid K = K
16 3 adantr φ x y dom lub K K V
17 simpr φ x y dom lub K x y dom lub K
18 1 15 5 16 17 lubelss φ x y dom lub K x y B
19 18 ex φ x y dom lub K x y B
20 10 12 prss x B y B x y B
21 opelxpi x B y B x y B × B
22 20 21 sylbir x y B x y B × B
23 19 22 syl6 φ x y dom lub K x y B × B
24 14 23 sylbid φ x y dom ˙ x y B × B
25 9 24 relssdv φ dom ˙ B × B