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 ) ) )