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

Metamath Proof Explorer

Theorem infiso

Description: Image of an infimum under an isomorphism. (Contributed by AV, 4-Sep-2020)

Ref Expression
Hypotheses infiso.1 
|- ( ph -> F Isom R , S ( A , B ) )
infiso.2 
|- ( ph -> C C_ A )
infiso.3 
|- ( ph -> E. x e. A ( A. y e. C -. y R x /\ A. y e. A ( x R y -> E. z e. C z R y ) ) )
infiso.4 
|- ( ph -> R Or A )
Assertion infiso 
|- ( ph -> inf ( ( F " C ) , B , S ) = ( F ` inf ( C , A , R ) ) )

Proof

Step Hyp Ref Expression
1 infiso.1 
 |-  ( ph -> F Isom R , S ( A , B ) )
2 infiso.2 
 |-  ( ph -> C C_ A )
3 infiso.3 
 |-  ( ph -> E. x e. A ( A. y e. C -. y R x /\ A. y e. A ( x R y -> E. z e. C z R y ) ) )
4 infiso.4 
 |-  ( ph -> R Or A )
5 isocnv2 
 |-  ( F Isom R , S ( A , B ) <-> F Isom `' R , `' S ( A , B ) )
6 1 5 sylib 
 |-  ( ph -> F Isom `' R , `' S ( A , B ) )
7 4 3 infcllem 
 |-  ( ph -> E. x e. A ( A. y e. C -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. C y `' R z ) ) )
8 cnvso 
 |-  ( R Or A <-> `' R Or A )
9 4 8 sylib 
 |-  ( ph -> `' R Or A )
10 6 2 7 9 supiso 
 |-  ( ph -> sup ( ( F " C ) , B , `' S ) = ( F ` sup ( C , A , `' R ) ) )
11 df-inf 
 |-  inf ( ( F " C ) , B , S ) = sup ( ( F " C ) , B , `' S )
12 df-inf 
 |-  inf ( C , A , R ) = sup ( C , A , `' R )
13 12 fveq2i 
 |-  ( F ` inf ( C , A , R ) ) = ( F ` sup ( C , A , `' R ) )
14 10 11 13 3eqtr4g 
 |-  ( ph -> inf ( ( F " C ) , B , S ) = ( F ` inf ( C , A , R ) ) )