Theorem infiso

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

	Ref	Expression
Hypotheses	infiso.1	$$⊢\phi \to F{Isom}_{R,S}\left(A,B\right)$$
	infiso.2	$$⊢\phi \to C\subseteq A$$
	infiso.3	$$⊢\phi \to \exists x\in A\left(\forall y\in C\neg yRx\wedge \forall y\in A\left(xRy\to \exists z\in CzRy\right)\right)$$
	infiso.4	$$⊢\phi \to R\mathrm{Or}A$$
Assertion	infiso	$$⊢\phi \to sup\left(F\left[C\right],B,S\right)=F\left(sup\left(C,A,R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		infiso.1	$$⊢\phi \to F{Isom}_{R,S}\left(A,B\right)$$
2		infiso.2	$$⊢\phi \to C\subseteq A$$
3		infiso.3	$$⊢\phi \to \exists x\in A\left(\forall y\in C\neg yRx\wedge \forall y\in A\left(xRy\to \exists z\in CzRy\right)\right)$$
4		infiso.4	$$⊢\phi \to R\mathrm{Or}A$$
5		isocnv2	$$⊢F{Isom}_{R,S}\left(A,B\right)\leftrightarrow F{Isom}_{R^{-1},S^{-1}}\left(A,B\right)$$
6	1 5	sylib	$$⊢\phi \to F{Isom}_{R^{-1},S^{-1}}\left(A,B\right)$$
7	4 3	infcllem	$$⊢\phi \to \exists x\in A\left(\forall y\in C\neg x{R}^{-1}y\wedge \forall y\in A\left(y{R}^{-1}x\to \exists z\in Cy{R}^{-1}z\right)\right)$$
8		cnvso	$$⊢R\mathrm{Or}A\leftrightarrow R^{-1}\mathrm{Or}A$$
9	4 8	sylib	$$⊢\phi \to R^{-1}\mathrm{Or}A$$
10	6 2 7 9	supiso	$$⊢\phi \to sup\left(F\left[C\right],B,S^{-1}\right)=F\left(sup\left(C,A,R^{-1}\right)\right)$$
11		df-inf	$$⊢sup\left(F\left[C\right],B,S\right)=sup\left(F\left[C\right],B,S^{-1}\right)$$
12		df-inf	$$⊢sup\left(C,A,R\right)=sup\left(C,A,R^{-1}\right)$$
13	12	fveq2i	$$⊢F\left(sup\left(C,A,R\right)\right)=F\left(sup\left(C,A,R^{-1}\right)\right)$$
14	10 11 13	3eqtr4g	$$⊢\phi \to sup\left(F\left[C\right],B,S\right)=F\left(sup\left(C,A,R\right)\right)$$