Metamath Proof Explorer

Theorem ipolub00

Description: The LUB of the empty set is the empty set if it is contained. (Contributed by Zhi Wang, 30-Sep-2024)

Ref Expression
Hypotheses ipoglb0.i ⊢ I = toInc ⁡ F
ipolub00.u ⊢ φ → U = lub ⁡ I
ipolub00.f ⊢ φ → ∅ ∈ F
Assertion ipolub00 ⊢ φ → U ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 ipoglb0.i ⊢ I = toInc ⁡ F
2 ipolub00.u ⊢ φ → U = lub ⁡ I
3 ipolub00.f ⊢ φ → ∅ ∈ F
4 2 adantr ⊢ φ ∧ F ∈ V → U = lub ⁡ I
5 int0el ⊢ ∅ ∈ F → ⋂ F = ∅
6 3 5 syl ⊢ φ → ⋂ F = ∅
7 6 3 eqeltrd ⊢ φ → ⋂ F ∈ F
8 7 adantr ⊢ φ ∧ F ∈ V → ⋂ F ∈ F
9 simpr ⊢ φ ∧ F ∈ V → F ∈ V
10 1 4 8 9 ipolub0 ⊢ φ ∧ F ∈ V → U ⁡ ∅ = ⋂ F
11 6 adantr ⊢ φ ∧ F ∈ V → ⋂ F = ∅
12 10 11 eqtrd ⊢ φ ∧ F ∈ V → U ⁡ ∅ = ∅
13 2 adantr ⊢ φ ∧ ¬ F ∈ V → U = lub ⁡ I
14 fvprc ⊢ ¬ F ∈ V → toInc ⁡ F = ∅
15 14 adantl ⊢ φ ∧ ¬ F ∈ V → toInc ⁡ F = ∅
16 1 15 syl5eq ⊢ φ ∧ ¬ F ∈ V → I = ∅
17 16 fveq2d ⊢ φ ∧ ¬ F ∈ V → lub ⁡ I = lub ⁡ ∅
18 13 17 eqtrd ⊢ φ ∧ ¬ F ∈ V → U = lub ⁡ ∅
19 18 fveq1d ⊢ φ ∧ ¬ F ∈ V → U ⁡ ∅ = lub ⁡ ∅ ⁡ ∅
20 rex0 ⊢ ¬ ∃ x ∈ ∅ ∀ y ∈ ∅ y ≤ ∅ x ∧ ∀ z ∈ ∅ ∀ y ∈ ∅ y ≤ ∅ z → x ≤ ∅ z
21 20 intnan ⊢ ¬ ∅ ⊆ ∅ ∧ ∃ x ∈ ∅ ∀ y ∈ ∅ y ≤ ∅ x ∧ ∀ z ∈ ∅ ∀ y ∈ ∅ y ≤ ∅ z → x ≤ ∅ z
22 base0 ⊢ ∅ = Base ∅
23 eqid ⊢ ≤ ∅ = ≤ ∅
24 eqid ⊢ lub ⁡ ∅ = lub ⁡ ∅
25 biid ⊢ ∀ y ∈ ∅ y ≤ ∅ x ∧ ∀ z ∈ ∅ ∀ y ∈ ∅ y ≤ ∅ z → x ≤ ∅ z ↔ ∀ y ∈ ∅ y ≤ ∅ x ∧ ∀ z ∈ ∅ ∀ y ∈ ∅ y ≤ ∅ z → x ≤ ∅ z
26 0pos ⊢ ∅ ∈ Poset
27 26 a1i ⊢ φ ∧ ¬ F ∈ V → ∅ ∈ Poset
28 22 23 24 25 27 lubeldm2 ⊢ φ ∧ ¬ F ∈ V → ∅ ∈ dom ⁡ lub ⁡ ∅ ↔ ∅ ⊆ ∅ ∧ ∃ x ∈ ∅ ∀ y ∈ ∅ y ≤ ∅ x ∧ ∀ z ∈ ∅ ∀ y ∈ ∅ y ≤ ∅ z → x ≤ ∅ z
29 21 28 mtbiri ⊢ φ ∧ ¬ F ∈ V → ¬ ∅ ∈ dom ⁡ lub ⁡ ∅
30 ndmfv ⊢ ¬ ∅ ∈ dom ⁡ lub ⁡ ∅ → lub ⁡ ∅ ⁡ ∅ = ∅
31 29 30 syl ⊢ φ ∧ ¬ F ∈ V → lub ⁡ ∅ ⁡ ∅ = ∅
32 19 31 eqtrd ⊢ φ ∧ ¬ F ∈ V → U ⁡ ∅ = ∅
33 12 32 pm2.61dan ⊢ φ → U ⁡ ∅ = ∅