MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1otrge Structured version   Visualization version   Unicode version
Theorem f1otrge 25752
Description: A bijection between bases which conserves distances and intervals conserves also the property of being a Euclidean geometry. (Contributed by Thierry Arnoux, 23-Mar-2019.)
Hypotheses
Ref Expression
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 ) ) ) )
f1otrg.h |- ( ph -> H e. V )
f1otrge.g |- ( ph -> G e. TarskiGE )
Assertion
Ref Expression
f1otrge |- ( ph -> H e. TarskiGE )
Distinct variable groups:   e, f, g, B   D, e, f, g   e, E, f, g   e, F, f, g   e, I, f, g   e, J, f, g   P, e, f, g   ph, e, f, g   f, H
Allowed substitution hints:   G( e, f, g)   H( e, g)   V( e, f, g)
Proof of Theorem f1otrge
Dummy variables a b c d u v x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1otrg.h . . 3 |- ( ph -> H e. V )
2 elex 3212 . . 3 |- ( H e. V -> H e. _V )
31, 2syl 17 . 2 |- ( ph -> H e. _V )
4 f1otrkg.f . . . . . . . . . 10 |- ( ph -> F : B -1-1-onto-> P )
5 f1ocnv 6149 . . . . . . . . . 10 |- ( F : B -1-1-onto-> P -> `' F : P -1-1-onto-> B )
6 f1of 6137 . . . . . . . . . 10 |- ( `' F : P -1-1-onto-> B -> `' F : P --> B )
74, 5, 63syl 18 . . . . . . . . 9 |- ( ph -> `' F : P --> B )
87ad6antr 772 . . . . . . . 8 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> `' F : P --> B )
9 simpllr 799 . . . . . . . 8 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> c e. P )
108, 9ffvelrnd 6360 . . . . . . 7 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( `' F ` c ) e. B )
11 simplr 792 . . . . . . . 8 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> d e. P )
128, 11ffvelrnd 6360 . . . . . . 7 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( `' F ` d ) e. B )
13 simpr1 1067 . . . . . . . . 9 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` y ) e. ( ( F ` x ) I c ) )
144ad3antrrr 766 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> F : B -1-1-onto-> P )
1514ad3antrrr 766 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> F : B -1-1-onto-> P )
16 f1ocnvfv2 6533 . . . . . . . . . . 11 |- ( ( F : B -1-1-onto-> P /\ c e. P ) -> ( F ` ( `' F ` c ) ) = c )
1715, 9, 16syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` ( `' F ` c ) ) = c )
1817oveq2d 6666 . . . . . . . . 9 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( ( F ` x ) I ( F ` ( `' F ` c ) ) ) = ( ( F ` x ) I c ) )
1913, 18eleqtrrd 2704 . . . . . . . 8 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` y ) e. ( ( F ` x ) I ( F ` ( `' F ` c ) ) ) )
20 f1otrkg.p . . . . . . . . 9 |- P = ( Base ` G )
21 f1otrkg.d . . . . . . . . 9 |- D = ( dist ` G )
22 f1otrkg.i . . . . . . . . 9 |- I = (Itv ` G )
23 f1otrkg.b . . . . . . . . 9 |- B = ( Base ` H )
24 f1otrkg.e . . . . . . . . 9 |- E = ( dist ` H )
25 f1otrkg.j . . . . . . . . 9 |- J = (Itv ` H )
26 simp-4l 806 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) /\ ( e e. B /\ f e. B ) ) -> ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) )
27 simplll 798 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ ( e e. B /\ f e. B ) ) -> ( ph /\ ( x e. B /\ y e. B ) ) )
28 f1otrkg.1 . . . . . . . . . . . 12 |- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
2928adantlr 751 . . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
3027, 29sylancom 701 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
3126, 30sylancom 701 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
32 simp-4l 806 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) )
33 simplll 798 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( ph /\ ( x e. B /\ y e. B ) ) )
34 f1otrkg.2 . . . . . . . . . . . 12 |- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
3534adantlr 751 . . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
3633, 35sylancom 701 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
3732, 36sylancom 701 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
38 simprl 794 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
3938ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> x e. B )
4039ad3antrrr 766 . . . . . . . . 9 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> x e. B )
41 simprr 796 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
4241ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> y e. B )
4342ad3antrrr 766 . . . . . . . . 9 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> y e. B )
4420, 21, 22, 23, 24, 25, 15, 31, 37, 40, 10, 43f1otrgitv 25750 . . . . . . . 8 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( y e. ( x J ( `' F ` c ) ) <-> ( F ` y ) e. ( ( F ` x ) I ( F ` ( `' F ` c ) ) ) ) )
4519, 44mpbird 247 . . . . . . 7 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> y e. ( x J ( `' F ` c ) ) )
46 simpr2 1068 . . . . . . . . 9 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` z ) e. ( ( F ` x ) I d ) )
47 f1ocnvfv2 6533 . . . . . . . . . . 11 |- ( ( F : B -1-1-onto-> P /\ d e. P ) -> ( F ` ( `' F ` d ) ) = d )
4815, 11, 47syl2anc 693 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` ( `' F ` d ) ) = d )
4948oveq2d 6666 . . . . . . . . 9 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( ( F ` x ) I ( F ` ( `' F ` d ) ) ) = ( ( F ` x ) I d ) )
5046, 49eleqtrrd 2704 . . . . . . . 8 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` z ) e. ( ( F ` x ) I ( F ` ( `' F ` d ) ) ) )
51 simplr1 1103 . . . . . . . . . 10 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> z e. B )
5251ad3antrrr 766 . . . . . . . . 9 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> z e. B )
5320, 21, 22, 23, 24, 25, 15, 31, 37, 40, 12, 52f1otrgitv 25750 . . . . . . . 8 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( z e. ( x J ( `' F ` d ) ) <-> ( F ` z ) e. ( ( F ` x ) I ( F ` ( `' F ` d ) ) ) ) )
5450, 53mpbird 247 . . . . . . 7 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> z e. ( x J ( `' F ` d ) ) )
55 simpr3 1069 . . . . . . . . 9 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` v ) e. ( c I d ) )
5617, 48oveq12d 6668 . . . . . . . . 9 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( ( F ` ( `' F ` c ) ) I ( F ` ( `' F ` d ) ) ) = ( c I d ) )
5755, 56eleqtrrd 2704 . . . . . . . 8 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` v ) e. ( ( F ` ( `' F ` c ) ) I ( F ` ( `' F ` d ) ) ) )
58 simplr3 1105 . . . . . . . . . 10 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> v e. B )
5958ad3antrrr 766 . . . . . . . . 9 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> v e. B )
6020, 21, 22, 23, 24, 25, 15, 31, 37, 10, 12, 59f1otrgitv 25750 . . . . . . . 8 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( v e. ( ( `' F ` c ) J ( `' F ` d ) ) <-> ( F ` v ) e. ( ( F ` ( `' F ` c ) ) I ( F ` ( `' F ` d ) ) ) ) )
6157, 60mpbird 247 . . . . . . 7 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> v e. ( ( `' F ` c ) J ( `' F ` d ) ) )
62 oveq2 6658 . . . . . . . . . 10 |- ( a = ( `' F ` c ) -> ( x J a ) = ( x J ( `' F ` c ) ) )
6362eleq2d 2687 . . . . . . . . 9 |- ( a = ( `' F ` c ) -> ( y e. ( x J a ) <-> y e. ( x J ( `' F ` c ) ) ) )
64 oveq1 6657 . . . . . . . . . 10 |- ( a = ( `' F ` c ) -> ( a J b ) = ( ( `' F ` c ) J b ) )
6564eleq2d 2687 . . . . . . . . 9 |- ( a = ( `' F ` c ) -> ( v e. ( a J b ) <-> v e. ( ( `' F ` c ) J b ) ) )
6663, 653anbi13d 1401 . . . . . . . 8 |- ( a = ( `' F ` c ) -> ( ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) <-> ( y e. ( x J ( `' F ` c ) ) /\ z e. ( x J b ) /\ v e. ( ( `' F ` c ) J b ) ) ) )
67 oveq2 6658 . . . . . . . . . 10 |- ( b = ( `' F ` d ) -> ( x J b ) = ( x J ( `' F ` d ) ) )
6867eleq2d 2687 . . . . . . . . 9 |- ( b = ( `' F ` d ) -> ( z e. ( x J b ) <-> z e. ( x J ( `' F ` d ) ) ) )
69 oveq2 6658 . . . . . . . . . 10 |- ( b = ( `' F ` d ) -> ( ( `' F ` c ) J b ) = ( ( `' F ` c ) J ( `' F ` d ) ) )
7069eleq2d 2687 . . . . . . . . 9 |- ( b = ( `' F ` d ) -> ( v e. ( ( `' F ` c ) J b ) <-> v e. ( ( `' F ` c ) J ( `' F ` d ) ) ) )
7168, 703anbi23d 1402 . . . . . . . 8 |- ( b = ( `' F ` d ) -> ( ( y e. ( x J ( `' F ` c ) ) /\ z e. ( x J b ) /\ v e. ( ( `' F ` c ) J b ) ) <-> ( y e. ( x J ( `' F ` c ) ) /\ z e. ( x J ( `' F ` d ) ) /\ v e. ( ( `' F ` c ) J ( `' F ` d ) ) ) ) )
7266, 71rspc2ev 3324 . . . . . . 7 |- ( ( ( `' F ` c ) e. B /\ ( `' F ` d ) e. B /\ ( y e. ( x J ( `' F ` c ) ) /\ z e. ( x J ( `' F ` d ) ) /\ v e. ( ( `' F ` c ) J ( `' F ` d ) ) ) ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) )
7310, 12, 45, 54, 61, 72syl113anc 1338 . . . . . 6 |- ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) )
74 f1otrge.g . . . . . . . 8 |- ( ph -> G e. TarskiGE )
7574ad3antrrr 766 . . . . . . 7 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> G e. TarskiGE )
76 f1of 6137 . . . . . . . . . . 11 |- ( F : B -1-1-onto-> P -> F : B --> P )
774, 76syl 17 . . . . . . . . . 10 |- ( ph -> F : B --> P )
7877adantr 481 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> F : B --> P )
7978, 38ffvelrnd 6360 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` x ) e. P )
8079ad2antrr 762 . . . . . . 7 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` x ) e. P )
8178, 41ffvelrnd 6360 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` y ) e. P )
8281ad2antrr 762 . . . . . . 7 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` y ) e. P )
8377ad3antrrr 766 . . . . . . . 8 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> F : B --> P )
8483, 51ffvelrnd 6360 . . . . . . 7 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` z ) e. P )
85 simplr2 1104 . . . . . . . 8 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> u e. B )
8683, 85ffvelrnd 6360 . . . . . . 7 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` u ) e. P )
8783, 58ffvelrnd 6360 . . . . . . 7 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` v ) e. P )
88 simpr1 1067 . . . . . . . 8 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> u e. ( x J v ) )
8920, 21, 22, 23, 24, 25, 14, 30, 36, 39, 58, 85f1otrgitv 25750 . . . . . . . 8 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( u e. ( x J v ) <-> ( F ` u ) e. ( ( F ` x ) I ( F ` v ) ) ) )
9088, 89mpbid 222 . . . . . . 7 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` u ) e. ( ( F ` x ) I ( F ` v ) ) )
91 simpr2 1068 . . . . . . . 8 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> u e. ( y J z ) )
9220, 21, 22, 23, 24, 25, 14, 30, 36, 42, 51, 85f1otrgitv 25750 . . . . . . . 8 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( u e. ( y J z ) <-> ( F ` u ) e. ( ( F ` y ) I ( F ` z ) ) ) )
9391, 92mpbid 222 . . . . . . 7 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` u ) e. ( ( F ` y ) I ( F ` z ) ) )
9414, 39jca 554 . . . . . . . 8 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F : B -1-1-onto-> P /\ x e. B ) )
95 simpr3 1069 . . . . . . . 8 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> x =/= u )
96 dff1o6 6531 . . . . . . . . . . . . 13 |- ( F : B -1-1-onto-> P <-> ( F Fn B /\ ran F = P /\ A. x e. B A. u e. B ( ( F ` x ) = ( F ` u ) -> x = u ) ) )
9796simp3bi 1078 . . . . . . . . . . . 12 |- ( F : B -1-1-onto-> P -> A. x e. B A. u e. B ( ( F ` x ) = ( F ` u ) -> x = u ) )
9897r19.21bi 2932 . . . . . . . . . . 11 |- ( ( F : B -1-1-onto-> P /\ x e. B ) -> A. u e. B ( ( F ` x ) = ( F ` u ) -> x = u ) )
9998r19.21bi 2932 . . . . . . . . . 10 |- ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ u e. B ) -> ( ( F ` x ) = ( F ` u ) -> x = u ) )
10099necon3d 2815 . . . . . . . . 9 |- ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ u e. B ) -> ( x =/= u -> ( F ` x ) =/= ( F ` u ) ) )
101100imp 445 . . . . . . . 8 |- ( ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ u e. B ) /\ x =/= u ) -> ( F ` x ) =/= ( F ` u ) )
10294, 85, 95, 101syl21anc 1325 . . . . . . 7 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` x ) =/= ( F ` u ) )
10320, 21, 22, 75, 80, 82, 84, 86, 87, 90, 93, 102axtgeucl 25371 . . . . . 6 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> E. c e. P E. d e. P ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) )
10473, 103r19.29vva 3081 . . . . 5 |- ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) )
105104ex 450 . . . 4 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) -> ( ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) ) )
106105ralrimivvva 2972 . . 3 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> A. z e. B A. u e. B A. v e. B ( ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) ) )
107106ralrimivva 2971 . 2 |- ( ph -> A. x e. B A. y e. B A. z e. B A. u e. B A. v e. B ( ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) ) )
10823, 24, 25istrkge 25356 . 2 |- ( H e. TarskiGE <-> ( H e. _V /\ A. x e. B A. y e. B A. z e. B A. u e. B A. v e. B ( ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) ) ) )
1093, 107, 108sylanbrc 698 1 |- ( ph -> H e. TarskiGE )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   `'ccnv 5113   ran crn 5115   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   Basecbs 15857   distcds 15950  TarskiGEcstrkge 25334  Itvcitv 25335
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-trkge 25350
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator