Theorem infiso

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

	Ref	Expression
Hypotheses	infiso.1	⊢ ( 𝜑 → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
	infiso.2	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
	infiso.3	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐶 𝑧 𝑅 𝑦 ) ) )
	infiso.4	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
Assertion	infiso	⊢ ( 𝜑 → inf ( ( 𝐹 “ 𝐶 ) , 𝐵 , 𝑆 ) = ( 𝐹 ‘ inf ( 𝐶 , 𝐴 , 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		infiso.1	⊢ ( 𝜑 → 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2		infiso.2	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3		infiso.3	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐶 𝑧 𝑅 𝑦 ) ) )
4		infiso.4	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
5		isocnv2	⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ◡ 𝑅 , ◡ 𝑆 ( 𝐴 , 𝐵 ) )
6	1 5	sylib	⊢ ( 𝜑 → 𝐹 Isom ◡ 𝑅 , ◡ 𝑆 ( 𝐴 , 𝐵 ) )
7	4 3	infcllem	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 ◡ 𝑅 𝑧 ) ) )
8		cnvso	⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
9	4 8	sylib	⊢ ( 𝜑 → ◡ 𝑅 Or 𝐴 )
10	6 2 7 9	supiso	⊢ ( 𝜑 → sup ( ( 𝐹 “ 𝐶 ) , 𝐵 , ◡ 𝑆 ) = ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , ◡ 𝑅 ) ) )
11		df-inf	⊢ inf ( ( 𝐹 “ 𝐶 ) , 𝐵 , 𝑆 ) = sup ( ( 𝐹 “ 𝐶 ) , 𝐵 , ◡ 𝑆 )
12		df-inf	⊢ inf ( 𝐶 , 𝐴 , 𝑅 ) = sup ( 𝐶 , 𝐴 , ◡ 𝑅 )
13	12	fveq2i	⊢ ( 𝐹 ‘ inf ( 𝐶 , 𝐴 , 𝑅 ) ) = ( 𝐹 ‘ sup ( 𝐶 , 𝐴 , ◡ 𝑅 ) )
14	10 11 13	3eqtr4g	⊢ ( 𝜑 → inf ( ( 𝐹 “ 𝐶 ) , 𝐵 , 𝑆 ) = ( 𝐹 ‘ inf ( 𝐶 , 𝐴 , 𝑅 ) ) )