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 ⁡ ∅ = 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 | ∃ x ∃ y ∃ z w = x y z ∧ x y lub ⁡ ∅ z
7 br0 ⊢ ¬ x y ∅ z
8 base0 ⊢ ∅ = Base ∅
9 eqid ⊢ ≤ ∅ = ≤ ∅
10 biid ⊢ ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y ↔ ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y
11 id ⊢ ∅ ∈ V → ∅ ∈ V
12 8 9 2 10 11 lubfval ⊢ ∅ ∈ V → lub ⁡ ∅ = w ∈ 𝒫 ∅ ⟼ ι z ∈ ∅ | ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y ↾ w | ∃! z ∈ ∅ ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y
13 1 12 ax-mp ⊢ lub ⁡ ∅ = w ∈ 𝒫 ∅ ⟼ ι z ∈ ∅ | ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y ↾ w | ∃! z ∈ ∅ ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y
14 reu0 ⊢ ¬ ∃! z ∈ ∅ ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y
15 14 abf ⊢ w | ∃! z ∈ ∅ ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y = ∅
16 15 reseq2i ⊢ w ∈ 𝒫 ∅ ⟼ ι z ∈ ∅ | ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y ↾ w | ∃! z ∈ ∅ ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y = w ∈ 𝒫 ∅ ⟼ ι z ∈ ∅ | ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y ↾ ∅
17 res0 ⊢ w ∈ 𝒫 ∅ ⟼ ι z ∈ ∅ | ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y ↾ ∅ = ∅
18 16 17 eqtri ⊢ w ∈ 𝒫 ∅ ⟼ ι z ∈ ∅ | ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ y ↾ w | ∃! z ∈ ∅ ∀ x ∈ w x ≤ ∅ z ∧ ∀ y ∈ ∅ ∀ x ∈ w x ≤ ∅ y → z ≤ ∅ 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 ⊢ ¬ ∃ z w = x y z ∧ x y lub ⁡ ∅ z
24 23 nex ⊢ ¬ ∃ y ∃ z w = x y z ∧ x y lub ⁡ ∅ z
25 24 nex ⊢ ¬ ∃ x ∃ y ∃ z w = x y z ∧ x y lub ⁡ ∅ z
26 25 abf ⊢ w | ∃ x ∃ y ∃ 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 ⁡ ∅ = ∅