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

Metamath Proof Explorer

Theorem ipolublem

Description: Lemma for ipolubdm and ipolub . (Contributed by Zhi Wang, 28-Sep-2024)

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

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 ipolublem.l 
 |-  .<_ = ( le ` I )
5 unissb 
 |-  ( U. S C_ X <-> A. y e. S y C_ X )
6 2 ad2antrr 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> F e. V )
7 3 ad2antrr 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> S C_ F )
8 simpr 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> y e. S )
9 7 8 sseldd 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> y e. F )
10 simplr 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> X e. F )
11 1 4 ipole 
 |-  ( ( F e. V /\ y e. F /\ X e. F ) -> ( y .<_ X <-> y C_ X ) )
12 6 9 10 11 syl3anc 
 |-  ( ( ( ph /\ X e. F ) /\ y e. S ) -> ( y .<_ X <-> y C_ X ) )
13 12 ralbidva 
 |-  ( ( ph /\ X e. F ) -> ( A. y e. S y .<_ X <-> A. y e. S y C_ X ) )
14 5 13 bitr4id 
 |-  ( ( ph /\ X e. F ) -> ( U. S C_ X <-> A. y e. S y .<_ X ) )
15 unissb 
 |-  ( U. S C_ z <-> A. y e. S y C_ z )
16 6 adantlr 
 |-  ( ( ( ( ph /\ X e. F ) /\ z e. F ) /\ y e. S ) -> F e. V )
17 9 adantlr 
 |-  ( ( ( ( ph /\ X e. F ) /\ z e. F ) /\ y e. S ) -> y e. F )
18 simplr 
 |-  ( ( ( ( ph /\ X e. F ) /\ z e. F ) /\ y e. S ) -> z e. F )
19 1 4 ipole 
 |-  ( ( F e. V /\ y e. F /\ z e. F ) -> ( y .<_ z <-> y C_ z ) )
20 16 17 18 19 syl3anc 
 |-  ( ( ( ( ph /\ X e. F ) /\ z e. F ) /\ y e. S ) -> ( y .<_ z <-> y C_ z ) )
21 20 ralbidva 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> ( A. y e. S y .<_ z <-> A. y e. S y C_ z ) )
22 15 21 bitr4id 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> ( U. S C_ z <-> A. y e. S y .<_ z ) )
23 2 ad2antrr 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> F e. V )
24 simplr 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> X e. F )
25 simpr 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> z e. F )
26 1 4 ipole 
 |-  ( ( F e. V /\ X e. F /\ z e. F ) -> ( X .<_ z <-> X C_ z ) )
27 23 24 25 26 syl3anc 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> ( X .<_ z <-> X C_ z ) )
28 27 bicomd 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> ( X C_ z <-> X .<_ z ) )
29 22 28 imbi12d 
 |-  ( ( ( ph /\ X e. F ) /\ z e. F ) -> ( ( U. S C_ z -> X C_ z ) <-> ( A. y e. S y .<_ z -> X .<_ z ) ) )
30 29 ralbidva 
 |-  ( ( ph /\ X e. F ) -> ( A. z e. F ( U. S C_ z -> X C_ z ) <-> A. z e. F ( A. y e. S y .<_ z -> X .<_ z ) ) )
31 14 30 anbi12d 
 |-  ( ( ph /\ X e. F ) -> ( ( U. S C_ X /\ A. z e. F ( U. S C_ z -> X C_ z ) ) <-> ( A. y e. S y .<_ X /\ A. z e. F ( A. y e. S y .<_ z -> X .<_ z ) ) ) )