# 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 ∅ ∈ V
2 eqid ( lub ‘ ∅ ) = ( lub ‘ ∅ )
3 eqid ( join ‘ ∅ ) = ( join ‘ ∅ )
4 2 3 joinfval ( ∅ ∈ V → ( join ‘ ∅ ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 } )
5 1 4 ax-mp ( join ‘ ∅ ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 }
6 df-oprab { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 } = { 𝑤 ∣ ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 ) }
7 br0 ¬ { 𝑥 , 𝑦 } ∅ 𝑧
8 base0 ∅ = ( Base ‘ ∅ )
9 eqid ( le ‘ ∅ ) = ( le ‘ ∅ )
10 biid ( ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) ↔ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) )
11 id ( ∅ ∈ V → ∅ ∈ V )
12 8 9 2 10 11 lubfval ( ∅ ∈ V → ( lub ‘ ∅ ) = ( ( 𝑤 ∈ 𝒫 ∅ ↦ ( 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ { 𝑤 ∣ ∃! 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) } ) )
13 1 12 ax-mp ( lub ‘ ∅ ) = ( ( 𝑤 ∈ 𝒫 ∅ ↦ ( 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ { 𝑤 ∣ ∃! 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) } )
14 reu0 ¬ ∃! 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) )
15 14 abf { 𝑤 ∣ ∃! 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) } = ∅
16 15 reseq2i ( ( 𝑤 ∈ 𝒫 ∅ ↦ ( 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ { 𝑤 ∣ ∃! 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) } ) = ( ( 𝑤 ∈ 𝒫 ∅ ↦ ( 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ ∅ )
17 res0 ( ( 𝑤 ∈ 𝒫 ∅ ↦ ( 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ ∅ ) = ∅
18 16 17 eqtri ( ( 𝑤 ∈ 𝒫 ∅ ↦ ( 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ { 𝑤 ∣ ∃! 𝑧 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑦 ∈ ∅ ( ∀ 𝑥𝑤 𝑥 ( le ‘ ∅ ) 𝑦𝑧 ( le ‘ ∅ ) 𝑦 ) ) } ) = ∅
19 13 18 eqtri ( lub ‘ ∅ ) = ∅
20 19 breqi ( { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 ↔ { 𝑥 , 𝑦 } ∅ 𝑧 )
21 7 20 mtbir ¬ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧
22 21 intnan ¬ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 )
23 22 nex ¬ ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 )
24 23 nex ¬ ∃ 𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 )
25 24 nex ¬ ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 )
26 25 abf { 𝑤 ∣ ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 ) } = ∅
27 6 26 eqtri { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( lub ‘ ∅ ) 𝑧 } = ∅
28 5 27 eqtri ( join ‘ ∅ ) = ∅