This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> U = ( lub ` I ) )
ipolub00.f 
|- ( ph -> (/) e. F )
Assertion ipolub00 
|- ( ph -> ( U ` (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 ipoglb0.i 
 |-  I = ( toInc ` F )
2 ipolub00.u 
 |-  ( ph -> U = ( lub ` I ) )
3 ipolub00.f 
 |-  ( ph -> (/) e. F )
4 2 adantr 
 |-  ( ( ph /\ F e. _V ) -> U = ( lub ` I ) )
5 int0el 
 |-  ( (/) e. F -> |^| F = (/) )
6 3 5 syl 
 |-  ( ph -> |^| F = (/) )
7 6 3 eqeltrd 
 |-  ( ph -> |^| F e. F )
8 7 adantr 
 |-  ( ( ph /\ F e. _V ) -> |^| F e. F )
9 simpr 
 |-  ( ( ph /\ F e. _V ) -> F e. _V )
10 1 4 8 9 ipolub0 
 |-  ( ( ph /\ F e. _V ) -> ( U ` (/) ) = |^| F )
11 6 adantr 
 |-  ( ( ph /\ F e. _V ) -> |^| F = (/) )
12 10 11 eqtrd 
 |-  ( ( ph /\ F e. _V ) -> ( U ` (/) ) = (/) )
13 2 adantr 
 |-  ( ( ph /\ -. F e. _V ) -> U = ( lub ` I ) )
14 fvprc 
 |-  ( -. F e. _V -> ( toInc ` F ) = (/) )
15 14 adantl 
 |-  ( ( ph /\ -. F e. _V ) -> ( toInc ` F ) = (/) )
16 1 15 eqtrid 
 |-  ( ( ph /\ -. F e. _V ) -> I = (/) )
17 16 fveq2d 
 |-  ( ( ph /\ -. F e. _V ) -> ( lub ` I ) = ( lub ` (/) ) )
18 13 17 eqtrd 
 |-  ( ( ph /\ -. F e. _V ) -> U = ( lub ` (/) ) )
19 18 fveq1d 
 |-  ( ( ph /\ -. F e. _V ) -> ( U ` (/) ) = ( ( lub ` (/) ) ` (/) ) )
20 rex0 
 |-  -. E. x e. (/) ( A. y e. (/) y ( le ` (/) ) x /\ A. z e. (/) ( A. y e. (/) y ( le ` (/) ) z -> x ( le ` (/) ) z ) )
21 20 intnan 
 |-  -. ( (/) C_ (/) /\ E. x e. (/) ( A. y e. (/) y ( le ` (/) ) x /\ A. z e. (/) ( A. y e. (/) y ( le ` (/) ) z -> x ( le ` (/) ) z ) ) )
22 base0 
 |-  (/) = ( Base ` (/) )
23 eqid 
 |-  ( le ` (/) ) = ( le ` (/) )
24 eqid 
 |-  ( lub ` (/) ) = ( lub ` (/) )
25 biid 
 |-  ( ( A. y e. (/) y ( le ` (/) ) x /\ A. z e. (/) ( A. y e. (/) y ( le ` (/) ) z -> x ( le ` (/) ) z ) ) <-> ( A. y e. (/) y ( le ` (/) ) x /\ A. z e. (/) ( A. y e. (/) y ( le ` (/) ) z -> x ( le ` (/) ) z ) ) )
26 0pos 
 |-  (/) e. Poset
27 26 a1i 
 |-  ( ( ph /\ -. F e. _V ) -> (/) e. Poset )
28 22 23 24 25 27 lubeldm2 
 |-  ( ( ph /\ -. F e. _V ) -> ( (/) e. dom ( lub ` (/) ) <-> ( (/) C_ (/) /\ E. x e. (/) ( A. y e. (/) y ( le ` (/) ) x /\ A. z e. (/) ( A. y e. (/) y ( le ` (/) ) z -> x ( le ` (/) ) z ) ) ) ) )
29 21 28 mtbiri 
 |-  ( ( ph /\ -. F e. _V ) -> -. (/) e. dom ( lub ` (/) ) )
30 ndmfv 
 |-  ( -. (/) e. dom ( lub ` (/) ) -> ( ( lub ` (/) ) ` (/) ) = (/) )
31 29 30 syl 
 |-  ( ( ph /\ -. F e. _V ) -> ( ( lub ` (/) ) ` (/) ) = (/) )
32 19 31 eqtrd 
 |-  ( ( ph /\ -. F e. _V ) -> ( U ` (/) ) = (/) )
33 12 32 pm2.61dan 
 |-  ( ph -> ( U ` (/) ) = (/) )