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 ` (/) ) = (/)