Metamath Proof Explorer

Theorem supiso

Description: Image of a supremum under an isomorphism. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses supiso.1 ⊢ φ → F Isom R , S A B
supiso.2 ⊢ φ → C ⊆ A
supisoex.3 ⊢ φ → ∃ x ∈ A ∀ y ∈ C ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ C y R z
supiso.4 ⊢ φ → R Or A
Assertion supiso ⊢ φ → sup F C B S = F ⁡ sup C A R

Proof

Step Hyp Ref Expression
1 supiso.1 ⊢ φ → F Isom R , S A B
2 supiso.2 ⊢ φ → C ⊆ A
3 supisoex.3 ⊢ φ → ∃ x ∈ A ∀ y ∈ C ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ C y R z
4 supiso.4 ⊢ φ → R Or A
5 isoso ⊢ F Isom R , S A B → R Or A ↔ S Or B
6 1 5 syl ⊢ φ → R Or A ↔ S Or B
7 4 6 mpbid ⊢ φ → S Or B
8 isof1o ⊢ F Isom R , S A B → F : A ⟶ 1-1 onto B
9 f1of ⊢ F : A ⟶ 1-1 onto B → F : A ⟶ B
10 1 8 9 3syl ⊢ φ → F : A ⟶ B
11 4 3 supcl ⊢ φ → sup C A R ∈ A
12 10 11 ffvelrnd ⊢ φ → F ⁡ sup C A R ∈ B
13 4 3 supub ⊢ φ → u ∈ C → ¬ sup C A R R u
14 13 ralrimiv ⊢ φ → ∀ u ∈ C ¬ sup C A R R u
15 4 3 suplub ⊢ φ → u ∈ A ∧ u R sup C A R → ∃ z ∈ C u R z
16 15 expd ⊢ φ → u ∈ A → u R sup C A R → ∃ z ∈ C u R z
17 16 ralrimiv ⊢ φ → ∀ u ∈ A u R sup C A R → ∃ z ∈ C u R z
18 1 2 supisolem ⊢ φ ∧ sup C A R ∈ A → ∀ u ∈ C ¬ sup C A R R u ∧ ∀ u ∈ A u R sup C A R → ∃ z ∈ C u R z ↔ ∀ w ∈ F C ¬ F ⁡ sup C A R S w ∧ ∀ w ∈ B w S F ⁡ sup C A R → ∃ v ∈ F C w S v
19 11 18 mpdan ⊢ φ → ∀ u ∈ C ¬ sup C A R R u ∧ ∀ u ∈ A u R sup C A R → ∃ z ∈ C u R z ↔ ∀ w ∈ F C ¬ F ⁡ sup C A R S w ∧ ∀ w ∈ B w S F ⁡ sup C A R → ∃ v ∈ F C w S v
20 14 17 19 mpbi2and ⊢ φ → ∀ w ∈ F C ¬ F ⁡ sup C A R S w ∧ ∀ w ∈ B w S F ⁡ sup C A R → ∃ v ∈ F C w S v
21 20 simpld ⊢ φ → ∀ w ∈ F C ¬ F ⁡ sup C A R S w
22 21 r19.21bi ⊢ φ ∧ w ∈ F C → ¬ F ⁡ sup C A R S w
23 20 simprd ⊢ φ → ∀ w ∈ B w S F ⁡ sup C A R → ∃ v ∈ F C w S v
24 23 r19.21bi ⊢ φ ∧ w ∈ B → w S F ⁡ sup C A R → ∃ v ∈ F C w S v
25 24 impr ⊢ φ ∧ w ∈ B ∧ w S F ⁡ sup C A R → ∃ v ∈ F C w S v
26 7 12 22 25 eqsupd ⊢ φ → sup F C B S = F ⁡ sup C A R