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 ⁡ ∅ = x y z | x y glb ⁡ ∅ z
5 1 4 ax-mp ⊢ meet ⁡ ∅ = x y z | x y glb ⁡ ∅ z
6 df-oprab ⊢ x y z | x y glb ⁡ ∅ z = w | ∃ x ∃ y ∃ z w = x y z ∧ x y glb ⁡ ∅ z
7 br0 ⊢ ¬ x y ∅ z
8 base0 ⊢ ∅ = Base ∅
9 eqid ⊢ ≤ ∅ = ≤ ∅
10 biid ⊢ ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y ↔ ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y
11 id ⊢ ∅ ∈ V → ∅ ∈ V
12 8 9 2 10 11 glbfval ⊢ ∅ ∈ V → glb ⁡ ∅ = x ∈ 𝒫 ∅ ⟼ ι y ∈ ∅ | ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y ↾ x | ∃! y ∈ ∅ ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y
13 1 12 ax-mp ⊢ glb ⁡ ∅ = x ∈ 𝒫 ∅ ⟼ ι y ∈ ∅ | ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y ↾ x | ∃! y ∈ ∅ ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y
14 reu0 ⊢ ¬ ∃! y ∈ ∅ ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y
15 14 abf ⊢ x | ∃! y ∈ ∅ ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y = ∅
16 15 reseq2i ⊢ x ∈ 𝒫 ∅ ⟼ ι y ∈ ∅ | ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y ↾ x | ∃! y ∈ ∅ ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y = x ∈ 𝒫 ∅ ⟼ ι y ∈ ∅ | ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y ↾ ∅
17 res0 ⊢ x ∈ 𝒫 ∅ ⟼ ι y ∈ ∅ | ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y ↾ ∅ = ∅
18 16 17 eqtri ⊢ x ∈ 𝒫 ∅ ⟼ ι y ∈ ∅ | ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y ↾ x | ∃! y ∈ ∅ ∀ z ∈ x y ≤ ∅ z ∧ ∀ w ∈ ∅ ∀ z ∈ x w ≤ ∅ z → w ≤ ∅ y = ∅
19 13 18 eqtri ⊢ glb ⁡ ∅ = ∅
20 19 breqi ⊢ x y glb ⁡ ∅ z ↔ x y ∅ z
21 7 20 mtbir ⊢ ¬ x y glb ⁡ ∅ z
22 21 intnan ⊢ ¬ w = x y z ∧ x y glb ⁡ ∅ z
23 22 nex ⊢ ¬ ∃ z w = x y z ∧ x y glb ⁡ ∅ z
24 23 nex ⊢ ¬ ∃ y ∃ z w = x y z ∧ x y glb ⁡ ∅ z
25 24 nex ⊢ ¬ ∃ x ∃ y ∃ z w = x y z ∧ x y glb ⁡ ∅ z
26 25 abf ⊢ w | ∃ x ∃ y ∃ z w = x y z ∧ x y glb ⁡ ∅ z = ∅
27 6 26 eqtri ⊢ x y z | x y glb ⁡ ∅ z = ∅
28 5 27 eqtri ⊢ meet ⁡ ∅ = ∅