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 ⊢φ→FIsomR,SAB
supiso.2 ⊢φ→C⊆A
supisoex.3 ⊢φ→∃x∈A∀y∈C¬xRy∧∀y∈AyRx→∃z∈CyRz
supiso.4 ⊢φ→ROrA
Assertion supiso ⊢φ→supFCBS=F⁡supCAR

Proof

Step Hyp Ref Expression
1 supiso.1 ⊢φ→FIsomR,SAB
2 supiso.2 ⊢φ→C⊆A
3 supisoex.3 ⊢φ→∃x∈A∀y∈C¬xRy∧∀y∈AyRx→∃z∈CyRz
4 supiso.4 ⊢φ→ROrA
5 isoso ⊢FIsomR,SAB→ROrA↔SOrB
6 1 5 syl ⊢φ→ROrA↔SOrB
7 4 6 mpbid ⊢φ→SOrB
8 isof1o ⊢FIsomR,SAB→F:A⟶1-1 ontoB
9 f1of ⊢F:A⟶1-1 ontoB→F:A⟶B
10 1 8 9 3syl ⊢φ→F:A⟶B
11 4 3 supcl ⊢φ→supCAR∈A
12 10 11 ffvelcdmd ⊢φ→F⁡supCAR∈B
13 4 3 supub ⊢φ→u∈C→¬supCARRu
14 13 ralrimiv ⊢φ→∀u∈C¬supCARRu
15 4 3 suplub ⊢φ→u∈A∧uRsupCAR→∃z∈CuRz
16 15 expd ⊢φ→u∈A→uRsupCAR→∃z∈CuRz
17 16 ralrimiv ⊢φ→∀u∈AuRsupCAR→∃z∈CuRz
18 1 2 supisolem ⊢φ∧supCAR∈A→∀u∈C¬supCARRu∧∀u∈AuRsupCAR→∃z∈CuRz↔∀w∈FC¬F⁡supCARSw∧∀w∈BwSF⁡supCAR→∃v∈FCwSv
19 11 18 mpdan ⊢φ→∀u∈C¬supCARRu∧∀u∈AuRsupCAR→∃z∈CuRz↔∀w∈FC¬F⁡supCARSw∧∀w∈BwSF⁡supCAR→∃v∈FCwSv
20 14 17 19 mpbi2and ⊢φ→∀w∈FC¬F⁡supCARSw∧∀w∈BwSF⁡supCAR→∃v∈FCwSv
21 20 simpld ⊢φ→∀w∈FC¬F⁡supCARSw
22 21 r19.21bi ⊢φ∧w∈FC→¬F⁡supCARSw
23 20 simprd ⊢φ→∀w∈BwSF⁡supCAR→∃v∈FCwSv
24 23 r19.21bi ⊢φ∧w∈B→wSF⁡supCAR→∃v∈FCwSv
25 24 impr ⊢φ∧w∈B∧wSF⁡supCAR→∃v∈FCwSv
26 7 12 22 25 eqsupd ⊢φ→supFCBS=F⁡supCAR