This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> F Isom R , S ( A , B ) )
supiso.2 
|- ( ph -> C C_ A )
supisoex.3 
|- ( ph -> E. x e. A ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) )
supiso.4 
|- ( ph -> R Or A )
Assertion supiso 
|- ( ph -> sup ( ( F " C ) , B , S ) = ( F ` sup ( C , A , R ) ) )

Proof

Step Hyp Ref Expression
1 supiso.1 
 |-  ( ph -> F Isom R , S ( A , B ) )
2 supiso.2 
 |-  ( ph -> C C_ A )
3 supisoex.3 
 |-  ( ph -> E. x e. A ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) )
4 supiso.4 
 |-  ( ph -> R Or A )
5 isoso 
 |-  ( F Isom R , S ( A , B ) -> ( R Or A <-> S Or B ) )
6 1 5 syl 
 |-  ( ph -> ( R Or A <-> S Or B ) )
7 4 6 mpbid 
 |-  ( ph -> 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 
 |-  ( ph -> F : A --> B )
11 4 3 supcl 
 |-  ( ph -> sup ( C , A , R ) e. A )
12 10 11 ffvelcdmd 
 |-  ( ph -> ( F ` sup ( C , A , R ) ) e. B )
13 4 3 supub 
 |-  ( ph -> ( u e. C -> -. sup ( C , A , R ) R u ) )
14 13 ralrimiv 
 |-  ( ph -> A. u e. C -. sup ( C , A , R ) R u )
15 4 3 suplub 
 |-  ( ph -> ( ( u e. A /\ u R sup ( C , A , R ) ) -> E. z e. C u R z ) )
16 15 expd 
 |-  ( ph -> ( u e. A -> ( u R sup ( C , A , R ) -> E. z e. C u R z ) ) )
17 16 ralrimiv 
 |-  ( ph -> A. u e. A ( u R sup ( C , A , R ) -> E. z e. C u R z ) )
18 1 2 supisolem 
 |-  ( ( ph /\ sup ( C , A , R ) e. A ) -> ( ( A. u e. C -. sup ( C , A , R ) R u /\ A. u e. A ( u R sup ( C , A , R ) -> E. z e. C u R z ) ) <-> ( A. w e. ( F " C ) -. ( F ` sup ( C , A , R ) ) S w /\ A. w e. B ( w S ( F ` sup ( C , A , R ) ) -> E. v e. ( F " C ) w S v ) ) ) )
19 11 18 mpdan 
 |-  ( ph -> ( ( A. u e. C -. sup ( C , A , R ) R u /\ A. u e. A ( u R sup ( C , A , R ) -> E. z e. C u R z ) ) <-> ( A. w e. ( F " C ) -. ( F ` sup ( C , A , R ) ) S w /\ A. w e. B ( w S ( F ` sup ( C , A , R ) ) -> E. v e. ( F " C ) w S v ) ) ) )
20 14 17 19 mpbi2and 
 |-  ( ph -> ( A. w e. ( F " C ) -. ( F ` sup ( C , A , R ) ) S w /\ A. w e. B ( w S ( F ` sup ( C , A , R ) ) -> E. v e. ( F " C ) w S v ) ) )
21 20 simpld 
 |-  ( ph -> A. w e. ( F " C ) -. ( F ` sup ( C , A , R ) ) S w )
22 21 r19.21bi 
 |-  ( ( ph /\ w e. ( F " C ) ) -> -. ( F ` sup ( C , A , R ) ) S w )
23 20 simprd 
 |-  ( ph -> A. w e. B ( w S ( F ` sup ( C , A , R ) ) -> E. v e. ( F " C ) w S v ) )
24 23 r19.21bi 
 |-  ( ( ph /\ w e. B ) -> ( w S ( F ` sup ( C , A , R ) ) -> E. v e. ( F " C ) w S v ) )
25 24 impr 
 |-  ( ( ph /\ ( w e. B /\ w S ( F ` sup ( C , A , R ) ) ) ) -> E. v e. ( F " C ) w S v )
26 7 12 22 25 eqsupd 
 |-  ( ph -> sup ( ( F " C ) , B , S ) = ( F ` sup ( C , A , R ) ) )