# Metamath Proof Explorer

## Theorem join0

Description: Lemma for odumeet . (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Assertion join0
`|- ( join ` (/) ) = (/)`

### Proof

Step Hyp Ref Expression
1 0ex
` |-  (/) e. _V`
2 eqid
` |-  ( lub ` (/) ) = ( lub ` (/) )`
3 eqid
` |-  ( join ` (/) ) = ( join ` (/) )`
4 2 3 joinfval
` |-  ( (/) e. _V -> ( join ` (/) ) = { <. <. x , y >. , z >. | { x , y } ( lub ` (/) ) z } )`
5 1 4 ax-mp
` |-  ( join ` (/) ) = { <. <. x , y >. , z >. | { x , y } ( lub ` (/) ) z }`
6 df-oprab
` |-  { <. <. x , y >. , z >. | { x , y } ( lub ` (/) ) z } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ { x , y } ( lub ` (/) ) z ) }`
7 br0
` |-  -. { x , y } (/) z`
8 base0
` |-  (/) = ( Base ` (/) )`
9 eqid
` |-  ( le ` (/) ) = ( le ` (/) )`
10 biid
` |-  ( ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) <-> ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) )`
11 id
` |-  ( (/) e. _V -> (/) e. _V )`
12 8 9 2 10 11 lubfval
` |-  ( (/) e. _V -> ( lub ` (/) ) = ( ( w e. ~P (/) |-> ( iota_ z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) ) ) |` { w | E! z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) } ) )`
13 1 12 ax-mp
` |-  ( lub ` (/) ) = ( ( w e. ~P (/) |-> ( iota_ z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) ) ) |` { w | E! z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) } )`
14 reu0
` |-  -. E! z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) )`
15 14 abf
` |-  { w | E! z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) } = (/)`
16 15 reseq2i
` |-  ( ( w e. ~P (/) |-> ( iota_ z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) ) ) |` { w | E! z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) } ) = ( ( w e. ~P (/) |-> ( iota_ z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) ) ) |` (/) )`
17 res0
` |-  ( ( w e. ~P (/) |-> ( iota_ z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) ) ) |` (/) ) = (/)`
18 16 17 eqtri
` |-  ( ( w e. ~P (/) |-> ( iota_ z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) ) ) |` { w | E! z e. (/) ( A. x e. w x ( le ` (/) ) z /\ A. y e. (/) ( A. x e. w x ( le ` (/) ) y -> z ( le ` (/) ) y ) ) } ) = (/)`
19 13 18 eqtri
` |-  ( lub ` (/) ) = (/)`
20 19 breqi
` |-  ( { x , y } ( lub ` (/) ) z <-> { x , y } (/) z )`
21 7 20 mtbir
` |-  -. { x , y } ( lub ` (/) ) z`
22 21 intnan
` |-  -. ( w = <. <. x , y >. , z >. /\ { x , y } ( lub ` (/) ) z )`
23 22 nex
` |-  -. E. z ( w = <. <. x , y >. , z >. /\ { x , y } ( lub ` (/) ) z )`
24 23 nex
` |-  -. E. y E. z ( w = <. <. x , y >. , z >. /\ { x , y } ( lub ` (/) ) z )`
25 24 nex
` |-  -. E. x E. y E. z ( w = <. <. x , y >. , z >. /\ { x , y } ( lub ` (/) ) z )`
26 25 abf
` |-  { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ { x , y } ( lub ` (/) ) z ) } = (/)`
27 6 26 eqtri
` |-  { <. <. x , y >. , z >. | { x , y } ( lub ` (/) ) z } = (/)`
28 5 27 eqtri
` |-  ( join ` (/) ) = (/)`