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

Metamath Proof Explorer

Theorem ipoglb0

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

Ref Expression
Hypotheses ipoglb0.i 
|- I = ( toInc ` F )
ipoglb0.g 
|- ( ph -> G = ( glb ` I ) )
ipoglb0.f 
|- ( ph -> U. F e. F )
Assertion ipoglb0 
|- ( ph -> ( G ` (/) ) = U. F )

Proof

Step Hyp Ref Expression
1 ipoglb0.i 
 |-  I = ( toInc ` F )
2 ipoglb0.g 
 |-  ( ph -> G = ( glb ` I ) )
3 ipoglb0.f 
 |-  ( ph -> U. F e. F )
4 uniexr 
 |-  ( U. F e. F -> F e. _V )
5 3 4 syl 
 |-  ( ph -> F e. _V )
6 0ss 
 |-  (/) C_ F
7 6 a1i 
 |-  ( ph -> (/) C_ F )
8 ssv 
 |-  x C_ _V
9 int0 
 |-  |^| (/) = _V
10 8 9 sseqtrri 
 |-  x C_ |^| (/)
11 10 a1i 
 |-  ( x e. F -> x C_ |^| (/) )
12 11 rabeqc 
 |-  { x e. F | x C_ |^| (/) } = F
13 12 unieqi 
 |-  U. { x e. F | x C_ |^| (/) } = U. F
14 13 eqcomi 
 |-  U. F = U. { x e. F | x C_ |^| (/) }
15 14 a1i 
 |-  ( ph -> U. F = U. { x e. F | x C_ |^| (/) } )
16 1 5 7 2 15 3 ipoglb 
 |-  ( ph -> ( G ` (/) ) = U. F )