Metamath Proof Explorer

Theorem supisoex

Description: Lemma for supiso . (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 ) ) )
Assertion supisoex 
|- ( ph -> E. u e. B ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) )

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 simpl 
 |-  ( ( F Isom R , S ( A , B ) /\ C C_ A ) -> F Isom R , S ( A , B ) )
5 simpr 
 |-  ( ( F Isom R , S ( A , B ) /\ C C_ A ) -> C C_ A )
6 4 5 supisolem 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ x e. A ) -> ( ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) <-> ( A. w e. ( F " C ) -. ( F ` x ) S w /\ A. w e. B ( w S ( F ` x ) -> E. v e. ( F " C ) w S v ) ) ) )
7 isof1o 
 |-  ( F Isom R , S ( A , B ) -> F : A -1-1-onto-> B )
8 f1of 
 |-  ( F : A -1-1-onto-> B -> F : A --> B )
9 4 7 8 3syl 
 |-  ( ( F Isom R , S ( A , B ) /\ C C_ A ) -> F : A --> B )
10 9 ffvelrnda 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ x e. A ) -> ( F ` x ) e. B )
11 breq1 
 |-  ( u = ( F ` x ) -> ( u S w <-> ( F ` x ) S w ) )
12 11 notbid 
 |-  ( u = ( F ` x ) -> ( -. u S w <-> -. ( F ` x ) S w ) )
13 12 ralbidv 
 |-  ( u = ( F ` x ) -> ( A. w e. ( F " C ) -. u S w <-> A. w e. ( F " C ) -. ( F ` x ) S w ) )
14 breq2 
 |-  ( u = ( F ` x ) -> ( w S u <-> w S ( F ` x ) ) )
15 14 imbi1d 
 |-  ( u = ( F ` x ) -> ( ( w S u -> E. v e. ( F " C ) w S v ) <-> ( w S ( F ` x ) -> E. v e. ( F " C ) w S v ) ) )
16 15 ralbidv 
 |-  ( u = ( F ` x ) -> ( A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) <-> A. w e. B ( w S ( F ` x ) -> E. v e. ( F " C ) w S v ) ) )
17 13 16 anbi12d 
 |-  ( u = ( F ` x ) -> ( ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) <-> ( A. w e. ( F " C ) -. ( F ` x ) S w /\ A. w e. B ( w S ( F ` x ) -> E. v e. ( F " C ) w S v ) ) ) )
18 17 rspcev 
 |-  ( ( ( F ` x ) e. B /\ ( A. w e. ( F " C ) -. ( F ` x ) S w /\ A. w e. B ( w S ( F ` x ) -> E. v e. ( F " C ) w S v ) ) ) -> E. u e. B ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) )
19 18 ex 
 |-  ( ( F ` x ) e. B -> ( ( A. w e. ( F " C ) -. ( F ` x ) S w /\ A. w e. B ( w S ( F ` x ) -> E. v e. ( F " C ) w S v ) ) -> E. u e. B ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) ) )
20 10 19 syl 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ x e. A ) -> ( ( A. w e. ( F " C ) -. ( F ` x ) S w /\ A. w e. B ( w S ( F ` x ) -> E. v e. ( F " C ) w S v ) ) -> E. u e. B ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) ) )
21 6 20 sylbid 
 |-  ( ( ( F Isom R , S ( A , B ) /\ C C_ A ) /\ x e. A ) -> ( ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) -> E. u e. B ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) ) )
22 21 rexlimdva 
 |-  ( ( F Isom R , S ( A , B ) /\ C C_ A ) -> ( 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 ) ) -> E. u e. B ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) ) )
23 1 2 22 syl2anc 
 |-  ( 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 ) ) -> E. u e. B ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) ) )
24 3 23 mpd 
 |-  ( ph -> E. u e. B ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) )