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 ⊢ 𝐼 = ( toInc ‘ 𝐹 )
ipolub00.u ⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐼 ) )
ipolub00.f ⊢ ( 𝜑 → ∅ ∈ 𝐹 )
Assertion ipolub00 ( 𝜑 → ( 𝑈 ‘ ∅ ) = ∅ )

Proof

Step Hyp Ref Expression
1 ipoglb0.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
2 ipolub00.u ⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐼 ) )
3 ipolub00.f ⊢ ( 𝜑 → ∅ ∈ 𝐹 )
4 2 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → 𝑈 = ( lub ‘ 𝐼 ) )
5 int0el ⊢ ( ∅ ∈ 𝐹 → ∩ 𝐹 = ∅ )
6 3 5 syl ⊢ ( 𝜑 → ∩ 𝐹 = ∅ )
7 6 3 eqeltrd ⊢ ( 𝜑 → ∩ 𝐹 ∈ 𝐹 )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ∩ 𝐹 ∈ 𝐹 )
9 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → 𝐹 ∈ V )
10 1 4 8 9 ipolub0 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ( 𝑈 ‘ ∅ ) = ∩ 𝐹 )
11 6 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ∩ 𝐹 = ∅ )
12 10 11 eqtrd ⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ( 𝑈 ‘ ∅ ) = ∅ )
13 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → 𝑈 = ( lub ‘ 𝐼 ) )
14 fvprc ⊢ ( ¬ 𝐹 ∈ V → ( toInc ‘ 𝐹 ) = ∅ )
15 14 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ( toInc ‘ 𝐹 ) = ∅ )
16 1 15 syl5eq ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → 𝐼 = ∅ )
17 16 fveq2d ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ( lub ‘ 𝐼 ) = ( lub ‘ ∅ ) )
18 13 17 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → 𝑈 = ( lub ‘ ∅ ) )
19 18 fveq1d ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ( 𝑈 ‘ ∅ ) = ( ( lub ‘ ∅ ) ‘ ∅ ) )
20 rex0 ⊢ ¬ ∃ 𝑥 ∈ ∅ ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ ∅ ) 𝑥 ∧ ∀ 𝑧 ∈ ∅ ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ ∅ ) 𝑧 → 𝑥 ( le ‘ ∅ ) 𝑧 ) )
21 20 intnan ⊢ ¬ ( ∅ ⊆ ∅ ∧ ∃ 𝑥 ∈ ∅ ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ ∅ ) 𝑥 ∧ ∀ 𝑧 ∈ ∅ ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ ∅ ) 𝑧 → 𝑥 ( le ‘ ∅ ) 𝑧 ) ) )
22 base0 ⊢ ∅ = ( Base ‘ ∅ )
23 eqid ⊢ ( le ‘ ∅ ) = ( le ‘ ∅ )
24 eqid ⊢ ( lub ‘ ∅ ) = ( lub ‘ ∅ )
25 biid ⊢ ( ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ ∅ ) 𝑥 ∧ ∀ 𝑧 ∈ ∅ ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ ∅ ) 𝑧 → 𝑥 ( le ‘ ∅ ) 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ ∅ ) 𝑥 ∧ ∀ 𝑧 ∈ ∅ ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ ∅ ) 𝑧 → 𝑥 ( le ‘ ∅ ) 𝑧 ) ) )
26 0pos ⊢ ∅ ∈ Poset
27 26 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ∅ ∈ Poset )
28 22 23 24 25 27 lubeldm2 ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ( ∅ ∈ dom ( lub ‘ ∅ ) ↔ ( ∅ ⊆ ∅ ∧ ∃ 𝑥 ∈ ∅ ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ ∅ ) 𝑥 ∧ ∀ 𝑧 ∈ ∅ ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ ∅ ) 𝑧 → 𝑥 ( le ‘ ∅ ) 𝑧 ) ) ) ) )
29 21 28 mtbiri ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ¬ ∅ ∈ dom ( lub ‘ ∅ ) )
30 ndmfv ⊢ ( ¬ ∅ ∈ dom ( lub ‘ ∅ ) → ( ( lub ‘ ∅ ) ‘ ∅ ) = ∅ )
31 29 30 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ( ( lub ‘ ∅ ) ‘ ∅ ) = ∅ )
32 19 31 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ( 𝑈 ‘ ∅ ) = ∅ )
33 12 32 pm2.61dan ⊢ ( 𝜑 → ( 𝑈 ‘ ∅ ) = ∅ )