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