Metamath Proof Explorer

Theorem f1otrgitv

Description: Convenient lemma for f1otrg . (Contributed by Thierry Arnoux, 19-Mar-2019)

Ref Expression
Hypotheses f1otrkg.p 
|- P = ( Base ` G )
f1otrkg.d 
|- D = ( dist ` G )
f1otrkg.i 
|- I = ( Itv ` G )
f1otrkg.b 
|- B = ( Base ` H )
f1otrkg.e 
|- E = ( dist ` H )
f1otrkg.j 
|- J = ( Itv ` H )
f1otrkg.f 
|- ( ph -> F : B -1-1-onto-> P )
f1otrkg.1 
|- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
f1otrkg.2 
|- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
f1otrgitv.x 
|- ( ph -> X e. B )
f1otrgitv.y 
|- ( ph -> Y e. B )
f1otrgitv.z 
|- ( ph -> Z e. B )
Assertion f1otrgitv 
|- ( ph -> ( Z e. ( X J Y ) <-> ( F ` Z ) e. ( ( F ` X ) I ( F ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 f1otrkg.p 
 |-  P = ( Base ` G )
2 f1otrkg.d 
 |-  D = ( dist ` G )
3 f1otrkg.i 
 |-  I = ( Itv ` G )
4 f1otrkg.b 
 |-  B = ( Base ` H )
5 f1otrkg.e 
 |-  E = ( dist ` H )
6 f1otrkg.j 
 |-  J = ( Itv ` H )
7 f1otrkg.f 
 |-  ( ph -> F : B -1-1-onto-> P )
8 f1otrkg.1 
 |-  ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
9 f1otrkg.2 
 |-  ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
10 f1otrgitv.x 
 |-  ( ph -> X e. B )
11 f1otrgitv.y 
 |-  ( ph -> Y e. B )
12 f1otrgitv.z 
 |-  ( ph -> Z e. B )
13 9 ralrimivvva 
 |-  ( ph -> A. e e. B A. f e. B A. g e. B ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
14 oveq1 
 |-  ( e = X -> ( e J f ) = ( X J f ) )
15 14 eleq2d 
 |-  ( e = X -> ( g e. ( e J f ) <-> g e. ( X J f ) ) )
16 fveq2 
 |-  ( e = X -> ( F ` e ) = ( F ` X ) )
17 16 oveq1d 
 |-  ( e = X -> ( ( F ` e ) I ( F ` f ) ) = ( ( F ` X ) I ( F ` f ) ) )
18 17 eleq2d 
 |-  ( e = X -> ( ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) <-> ( F ` g ) e. ( ( F ` X ) I ( F ` f ) ) ) )
19 15 18 bibi12d 
 |-  ( e = X -> ( ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) <-> ( g e. ( X J f ) <-> ( F ` g ) e. ( ( F ` X ) I ( F ` f ) ) ) ) )
20 oveq2 
 |-  ( f = Y -> ( X J f ) = ( X J Y ) )
21 20 eleq2d 
 |-  ( f = Y -> ( g e. ( X J f ) <-> g e. ( X J Y ) ) )
22 fveq2 
 |-  ( f = Y -> ( F ` f ) = ( F ` Y ) )
23 22 oveq2d 
 |-  ( f = Y -> ( ( F ` X ) I ( F ` f ) ) = ( ( F ` X ) I ( F ` Y ) ) )
24 23 eleq2d 
 |-  ( f = Y -> ( ( F ` g ) e. ( ( F ` X ) I ( F ` f ) ) <-> ( F ` g ) e. ( ( F ` X ) I ( F ` Y ) ) ) )
25 21 24 bibi12d 
 |-  ( f = Y -> ( ( g e. ( X J f ) <-> ( F ` g ) e. ( ( F ` X ) I ( F ` f ) ) ) <-> ( g e. ( X J Y ) <-> ( F ` g ) e. ( ( F ` X ) I ( F ` Y ) ) ) ) )
26 eleq1 
 |-  ( g = Z -> ( g e. ( X J Y ) <-> Z e. ( X J Y ) ) )
27 fveq2 
 |-  ( g = Z -> ( F ` g ) = ( F ` Z ) )
28 27 eleq1d 
 |-  ( g = Z -> ( ( F ` g ) e. ( ( F ` X ) I ( F ` Y ) ) <-> ( F ` Z ) e. ( ( F ` X ) I ( F ` Y ) ) ) )
29 26 28 bibi12d 
 |-  ( g = Z -> ( ( g e. ( X J Y ) <-> ( F ` g ) e. ( ( F ` X ) I ( F ` Y ) ) ) <-> ( Z e. ( X J Y ) <-> ( F ` Z ) e. ( ( F ` X ) I ( F ` Y ) ) ) ) )
30 19 25 29 rspc3v 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( A. e e. B A. f e. B A. g e. B ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) -> ( Z e. ( X J Y ) <-> ( F ` Z ) e. ( ( F ` X ) I ( F ` Y ) ) ) ) )
31 10 11 12 30 syl3anc 
 |-  ( ph -> ( A. e e. B A. f e. B A. g e. B ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) -> ( Z e. ( X J Y ) <-> ( F ` Z ) e. ( ( F ` X ) I ( F ` Y ) ) ) ) )
32 13 31 mpd 
 |-  ( ph -> ( Z e. ( X J Y ) <-> ( F ` Z ) e. ( ( F ` X ) I ( F ` Y ) ) ) )