This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem meet0

Description: Lemma for odujoin . (Contributed by Stefan O'Rear, 29-Jan-2015) TODO ( df-riota update): This proof increased from 152 bytes to 547 bytes after the df-riota change. Any way to shorten it? join0 also.

Ref Expression
Assertion meet0 ( meet ‘ ∅ ) = ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 eqid ⊢ ( glb ‘ ∅ ) = ( glb ‘ ∅ )
3 eqid ⊢ ( meet ‘ ∅ ) = ( meet ‘ ∅ )
4 2 3 meetfval ⊢ ( ∅ ∈ V → ( meet ‘ ∅ ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 } )
5 1 4 ax-mp ⊢ ( meet ‘ ∅ ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 }
6 df-oprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 ) }
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 glbfval ⊢ ( ∅ ∈ V → ( glb ‘ ∅ ) = ( ( 𝑥 ∈ 𝒫 ∅ ↦ ( ℩ 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ { 𝑥 ∣ ∃! 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) } ) )
13 1 12 ax-mp ⊢ ( glb ‘ ∅ ) = ( ( 𝑥 ∈ 𝒫 ∅ ↦ ( ℩ 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( 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 ⊢ ( glb ‘ ∅ ) = ∅
20 19 breqi ⊢ ( { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 ↔ { 𝑥 , 𝑦 } ∅ 𝑧 )
21 7 20 mtbir ⊢ ¬ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧
22 21 intnan ⊢ ¬ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 )
23 22 nex ⊢ ¬ ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 )
24 23 nex ⊢ ¬ ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 )
25 24 nex ⊢ ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 )
26 25 abf ⊢ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 ) } = ∅
27 6 26 eqtri ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 } = ∅
28 5 27 eqtri ⊢ ( meet ‘ ∅ ) = ∅