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 ⊢ φ → F Isom R , S A B
infiso.2 ⊢ φ → C ⊆ A
infiso.3 ⊢ φ → ∃ x ∈ A ∀ y ∈ C ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ C z R y
infiso.4 ⊢ φ → R Or A
Assertion infiso ⊢ φ → inf F C B S = F ⁡ inf C A R

Proof

Step Hyp Ref Expression
1 infiso.1 ⊢ φ → F Isom R , S A B
2 infiso.2 ⊢ φ → C ⊆ A
3 infiso.3 ⊢ φ → ∃ x ∈ A ∀ y ∈ C ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ C z R y
4 infiso.4 ⊢ φ → R Or A
5 isocnv2 ⊢ F Isom R , S A B ↔ F Isom R -1 , S -1 A B
6 1 5 sylib ⊢ φ → F Isom R -1 , S -1 A B
7 4 3 infcllem ⊢ φ → ∃ x ∈ A ∀ y ∈ C ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ C y R -1 z
8 cnvso ⊢ R Or A ↔ R -1 Or A
9 4 8 sylib ⊢ φ → R -1 Or A
10 6 2 7 9 supiso ⊢ φ → sup F C B S -1 = F ⁡ sup C A R -1
11 df-inf ⊢ inf F C B S = sup F C B S -1
12 df-inf ⊢ inf C A R = sup C A R -1
13 12 fveq2i ⊢ F ⁡ inf C A R = F ⁡ sup C A R -1
14 10 11 13 3eqtr4g ⊢ φ → inf F C B S = F ⁡ inf C A R