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

Metamath Proof Explorer

Theorem ipolub0

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

Ref Expression
Hypotheses ipoglb0.i 
|- I = ( toInc ` F )
ipolub0.u 
|- ( ph -> U = ( lub ` I ) )
ipolub0.f 
|- ( ph -> |^| F e. F )
ipolub0.v 
|- ( ph -> F e. V )
Assertion ipolub0 
|- ( ph -> ( U ` (/) ) = |^| F )

Proof

Step Hyp Ref Expression
1 ipoglb0.i 
 |-  I = ( toInc ` F )
2 ipolub0.u 
 |-  ( ph -> U = ( lub ` I ) )
3 ipolub0.f 
 |-  ( ph -> |^| F e. F )
4 ipolub0.v 
 |-  ( ph -> F e. V )
5 0ss 
 |-  (/) C_ F
6 5 a1i 
 |-  ( ph -> (/) C_ F )
7 uni0 
 |-  U. (/) = (/)
8 0ss 
 |-  (/) C_ x
9 7 8 eqsstri 
 |-  U. (/) C_ x
10 9 a1i 
 |-  ( x e. F -> U. (/) C_ x )
11 10 rabeqc 
 |-  { x e. F | U. (/) C_ x } = F
12 11 eqcomi 
 |-  F = { x e. F | U. (/) C_ x }
13 12 inteqi 
 |-  |^| F = |^| { x e. F | U. (/) C_ x }
14 13 a1i 
 |-  ( ph -> |^| F = |^| { x e. F | U. (/) C_ x } )
15 1 4 6 2 14 3 ipolub 
 |-  ( ph -> ( U ` (/) ) = |^| F )