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

Metamath Proof Explorer

Theorem ipoglblem

Description: Lemma for ipoglbdm and ipoglb . (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Hypotheses ipolub.i 
|- I = ( toInc ` F )
ipolub.f 
|- ( ph -> F e. V )
ipolub.s 
|- ( ph -> S C_ F )
ipoglblem.l 
|- .<_ = ( le ` I )
Assertion ipoglblem 
|- ( ( ph /\ X e. F ) -> ( ( X C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ X ) ) <-> ( A. y e. S X .<_ y /\ A. z e. F ( A. y e. S z .<_ y -> z .<_ X ) ) ) )

Proof

Step Hyp Ref Expression
1 ipolub.i 
 |-  I = ( toInc ` F )
2 ipolub.f 
 |-  ( ph -> F e. V )
3 ipolub.s 
 |-  ( ph -> S C_ F )
4 ipoglblem.l 
 |-  .<_ = ( le ` I )
5 ssint 
 |-  ( X C_ |^| S <-> A. y e. S X C_ y )
6 2 ad2antrr 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> F e. V )
7 simplr 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> X e. F )
8 3 ad2antrr 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> S C_ F )
9 simpr 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> y e. S )
10 8 9 sseldd 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> y e. F )
11 1 4 ipole 
 |-  ( ( F e. V /\ X e. F /\ y e. F ) -> ( X .<_ y <-> X C_ y ) )
12 6 7 10 11 syl3anc 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> ( X .<_ y <-> X C_ y ) )
13 12 ralbidva 
 |-  ( ( ph /\ X e. F ) -> ( A. y e. S X .<_ y <-> A. y e. S X C_ y ) )
14 5 13 bitr4id 
 |-  ( ( ph /\ X e. F ) -> ( X C_ |^| S <-> A. y e. S X .<_ y ) )
15 ssint 
 |-  ( z C_ |^| S <-> A. y e. S z C_ y )
16 6 adantlr 
 |-  ( ( ( ( ph /\ X e. F ) /\ z e. F ) /\ y e. S ) -> F e. V )
17 simplr 
 |-  ( ( ( ( ph /\ X e. F ) /\ z e. F ) /\ y e. S ) -> z e. F )
18 10 adantlr 
 |-  ( ( ( ( ph /\ X e. F ) /\ z e. F ) /\ y e. S ) -> y e. F )
19 1 4 ipole 
 |-  ( ( F e. V /\ z e. F /\ y e. F ) -> ( z .<_ y <-> z C_ y ) )
20 16 17 18 19 syl3anc 
 |-  ( ( ( ( ph /\ X e. F ) /\ z e. F ) /\ y e. S ) -> ( z .<_ y <-> z C_ y ) )
21 20 ralbidva 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> ( A. y e. S z .<_ y <-> A. y e. S z C_ y ) )
22 15 21 bitr4id 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> ( z C_ |^| S <-> A. y e. S z .<_ y ) )
23 2 ad2antrr 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> F e. V )
24 simpr 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> z e. F )
25 simplr 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> X e. F )
26 1 4 ipole 
 |-  ( ( F e. V /\ z e. F /\ X e. F ) -> ( z .<_ X <-> z C_ X ) )
27 23 24 25 26 syl3anc 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> ( z .<_ X <-> z C_ X ) )
28 27 bicomd 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> ( z C_ X <-> z .<_ X ) )
29 22 28 imbi12d 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> ( ( z C_ |^| S -> z C_ X ) <-> ( A. y e. S z .<_ y -> z .<_ X ) ) )
30 29 ralbidva 
 |-  ( ( ph /\ X e. F ) -> ( A. z e. F ( z C_ |^| S -> z C_ X ) <-> A. z e. F ( A. y e. S z .<_ y -> z .<_ X ) ) )
31 14 30 anbi12d 
 |-  ( ( ph /\ X e. F ) -> ( ( X C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ X ) ) <-> ( A. y e. S X .<_ y /\ A. z e. F ( A. y e. S z .<_ y -> z .<_ X ) ) ) )