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 ⊢ ( 𝜑 → 𝐹 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 ( 𝐶 , 𝐴 , 𝑅 ) ) )