ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  enq0tr Unicode version

Theorem enq0tr 7463
Description: The equivalence relation for nonnegative fractions is transitive. Lemma for enq0er 7464. (Contributed by Jim Kingdon, 14-Nov-2019.)
Assertion
Ref Expression
enq0tr  |-  ( ( f ~Q0  g  /\  g ~Q0  h )  ->  f ~Q0  h )

Proof of Theorem enq0tr
Dummy variables  a  b  c  d  e  s  t  u  v  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2755 . . . . . . . . . 10  |-  f  e. 
_V
2 vex 2755 . . . . . . . . . 10  |-  g  e. 
_V
3 eleq1 2252 . . . . . . . . . . . 12  |-  ( x  =  f  ->  (
x  e.  ( om 
X.  N. )  <->  f  e.  ( om  X.  N. )
) )
43anbi1d 465 . . . . . . . . . . 11  |-  ( x  =  f  ->  (
( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  <-> 
( f  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) ) ) )
5 eqeq1 2196 . . . . . . . . . . . . . 14  |-  ( x  =  f  ->  (
x  =  <. z ,  w >.  <->  f  =  <. z ,  w >. )
)
65anbi1d 465 . . . . . . . . . . . . 13  |-  ( x  =  f  ->  (
( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  <->  ( f  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. ) ) )
76anbi1d 465 . . . . . . . . . . . 12  |-  ( x  =  f  ->  (
( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  <->  ( (
f  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) ) ) )
874exbidv 1881 . . . . . . . . . . 11  |-  ( x  =  f  ->  ( E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  <->  E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) ) )
94, 8anbi12d 473 . . . . . . . . . 10  |-  ( x  =  f  ->  (
( ( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. )
)  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  <->  ( ( f  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) ) ) )
10 eleq1 2252 . . . . . . . . . . . 12  |-  ( y  =  g  ->  (
y  e.  ( om 
X.  N. )  <->  g  e.  ( om  X.  N. )
) )
1110anbi2d 464 . . . . . . . . . . 11  |-  ( y  =  g  ->  (
( f  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  <-> 
( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) ) ) )
12 eqeq1 2196 . . . . . . . . . . . . . 14  |-  ( y  =  g  ->  (
y  =  <. v ,  u >.  <->  g  =  <. v ,  u >. )
)
1312anbi2d 464 . . . . . . . . . . . . 13  |-  ( y  =  g  ->  (
( f  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  <->  ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. ) ) )
1413anbi1d 465 . . . . . . . . . . . 12  |-  ( y  =  g  ->  (
( ( f  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  <->  ( (
f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) ) ) )
15144exbidv 1881 . . . . . . . . . . 11  |-  ( y  =  g  ->  ( E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  <->  E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) ) )
1611, 15anbi12d 473 . . . . . . . . . 10  |-  ( y  =  g  ->  (
( ( f  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. )
)  /\  E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  <->  ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) ) ) )
17 df-enq0 7453 . . . . . . . . . 10  |- ~Q0  =  { <. x ,  y >.  |  ( ( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) ) }
181, 2, 9, 16, 17brab 4290 . . . . . . . . 9  |-  ( f ~Q0  g  <->  ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) ) )
19 vex 2755 . . . . . . . . . 10  |-  h  e. 
_V
20 eleq1 2252 . . . . . . . . . . . 12  |-  ( x  =  g  ->  (
x  e.  ( om 
X.  N. )  <->  g  e.  ( om  X.  N. )
) )
2120anbi1d 465 . . . . . . . . . . 11  |-  ( x  =  g  ->  (
( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  <-> 
( g  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) ) ) )
22 eqeq1 2196 . . . . . . . . . . . . . 14  |-  ( x  =  g  ->  (
x  =  <. a ,  b >.  <->  g  =  <. a ,  b >.
) )
2322anbi1d 465 . . . . . . . . . . . . 13  |-  ( x  =  g  ->  (
( x  =  <. a ,  b >.  /\  y  =  <. s ,  t
>. )  <->  ( g  = 
<. a ,  b >.  /\  y  =  <. s ,  t >. )
) )
2423anbi1d 465 . . . . . . . . . . . 12  |-  ( x  =  g  ->  (
( ( x  = 
<. a ,  b >.  /\  y  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) )  <-> 
( ( g  = 
<. a ,  b >.  /\  y  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )
25244exbidv 1881 . . . . . . . . . . 11  |-  ( x  =  g  ->  ( E. a E. b E. s E. t ( ( x  =  <. a ,  b >.  /\  y  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) )  <->  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  y  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )
2621, 25anbi12d 473 . . . . . . . . . 10  |-  ( x  =  g  ->  (
( ( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. )
)  /\  E. a E. b E. s E. t ( ( x  =  <. a ,  b
>.  /\  y  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  <->  ( ( g  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  y  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) ) )
27 eleq1 2252 . . . . . . . . . . . 12  |-  ( y  =  h  ->  (
y  e.  ( om 
X.  N. )  <->  h  e.  ( om  X.  N. )
) )
2827anbi2d 464 . . . . . . . . . . 11  |-  ( y  =  h  ->  (
( g  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  <-> 
( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) ) ) )
29 eqeq1 2196 . . . . . . . . . . . . . 14  |-  ( y  =  h  ->  (
y  =  <. s ,  t >.  <->  h  =  <. s ,  t >.
) )
3029anbi2d 464 . . . . . . . . . . . . 13  |-  ( y  =  h  ->  (
( g  =  <. a ,  b >.  /\  y  =  <. s ,  t
>. )  <->  ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )
) )
3130anbi1d 465 . . . . . . . . . . . 12  |-  ( y  =  h  ->  (
( ( g  = 
<. a ,  b >.  /\  y  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) )  <-> 
( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )
32314exbidv 1881 . . . . . . . . . . 11  |-  ( y  =  h  ->  ( E. a E. b E. s E. t ( ( g  =  <. a ,  b >.  /\  y  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) )  <->  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )
3328, 32anbi12d 473 . . . . . . . . . 10  |-  ( y  =  h  ->  (
( ( g  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. )
)  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  y  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  <->  ( ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) ) )
34 df-enq0 7453 . . . . . . . . . 10  |- ~Q0  =  { <. x ,  y >.  |  ( ( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  E. a E. b E. s E. t ( ( x  =  <. a ,  b
>.  /\  y  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) }
352, 19, 26, 33, 34brab 4290 . . . . . . . . 9  |-  ( g ~Q0  h  <->  ( ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )
3618, 35anbi12i 460 . . . . . . . 8  |-  ( ( f ~Q0  g  /\  g ~Q0  h )  <->  ( (
( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  /\  ( ( g  e.  ( om 
X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) ) )
3736biimpi 120 . . . . . . 7  |-  ( ( f ~Q0  g  /\  g ~Q0  h )  ->  (
( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )
)  /\  E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  /\  ( ( g  e.  ( om 
X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) ) )
38 an4 586 . . . . . . 7  |-  ( ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )
)  /\  E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  /\  ( ( g  e.  ( om 
X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  <->  ( (
( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) )  /\  ( E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) ) )
3937, 38sylib 122 . . . . . 6  |-  ( ( f ~Q0  g  /\  g ~Q0  h )  ->  (
( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )
)  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) )  /\  ( E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) ) )
40 3anass 984 . . . . . . . 8  |-  ( ( f  e.  ( om 
X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  <->  ( f  e.  ( om  X.  N. )  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) ) )
41 anass 401 . . . . . . . . 9  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) )  <->  ( f  e.  ( om  X.  N. )  /\  ( g  e.  ( om  X.  N. )  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) ) ) )
42 anass 401 . . . . . . . . . 10  |-  ( ( ( g  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  h  e.  ( om  X.  N. )
)  <->  ( g  e.  ( om  X.  N. )  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) ) )
4342anbi2i 457 . . . . . . . . 9  |-  ( ( f  e.  ( om 
X.  N. )  /\  (
( g  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  h  e.  ( om  X.  N. )
) )  <->  ( f  e.  ( om  X.  N. )  /\  ( g  e.  ( om  X.  N. )  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) ) ) )
44 anidm 396 . . . . . . . . . . 11  |-  ( ( g  e.  ( om 
X.  N. )  /\  g  e.  ( om  X.  N. ) )  <->  g  e.  ( om  X.  N. )
)
4544anbi1i 458 . . . . . . . . . 10  |-  ( ( ( g  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  h  e.  ( om  X.  N. )
)  <->  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) )
4645anbi2i 457 . . . . . . . . 9  |-  ( ( f  e.  ( om 
X.  N. )  /\  (
( g  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  h  e.  ( om  X.  N. )
) )  <->  ( f  e.  ( om  X.  N. )  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) ) )
4741, 43, 463bitr2i 208 . . . . . . . 8  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) )  <->  ( f  e.  ( om  X.  N. )  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) ) )
4840, 47bitr4i 187 . . . . . . 7  |-  ( ( f  e.  ( om 
X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  <->  ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  (
g  e.  ( om 
X.  N. )  /\  h  e.  ( om  X.  N. ) ) ) )
4948anbi1i 458 . . . . . 6  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  <->  ( (
( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. ) )  /\  ( g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) )  /\  ( E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) ) )
5039, 49sylibr 134 . . . . 5  |-  ( ( f ~Q0  g  /\  g ~Q0  h )  ->  (
( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) ) )
51 ee8anv 1947 . . . . . 6  |-  ( E. z E. w E. v E. u E. a E. b E. s E. t ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) )  <-> 
( E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )
5251anbi2i 457 . . . . 5  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. z E. w E. v E. u E. a E. b E. s E. t ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  <->  ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  ( E. z E. w E. v E. u ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  E. a E. b E. s E. t ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) ) )
5350, 52sylibr 134 . . . 4  |-  ( ( f ~Q0  g  /\  g ~Q0  h )  ->  (
( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. z E. w E. v E. u E. a E. b E. s E. t ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) ) )
54 19.42vvvv 1925 . . . . . . 7  |-  ( E. a E. b E. s E. t ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  <->  ( (
f  e.  ( om 
X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  E. a E. b E. s E. t ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) ) )
55542exbii 1617 . . . . . 6  |-  ( E. v E. u E. a E. b E. s E. t ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  ( (
( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  <->  E. v E. u
( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. a E. b E. s E. t ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) ) )
56552exbii 1617 . . . . 5  |-  ( E. z E. w E. v E. u E. a E. b E. s E. t ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  ( (
( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  <->  E. z E. w E. v E. u ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. a E. b E. s E. t ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) ) )
57 19.42vvvv 1925 . . . . 5  |-  ( E. z E. w E. v E. u ( ( f  e.  ( om 
X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  E. a E. b E. s E. t ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  <->  ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  E. z E. w E. v E. u E. a E. b E. s E. t ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) ) )
5856, 57bitri 184 . . . 4  |-  ( E. z E. w E. v E. u E. a E. b E. s E. t ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  ( (
( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  <->  ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  E. z E. w E. v E. u E. a E. b E. s E. t ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) ) )
5953, 58sylibr 134 . . 3  |-  ( ( f ~Q0  g  /\  g ~Q0  h )  ->  E. z E. w E. v E. u E. a E. b E. s E. t ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  ( (
( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) ) )
60 3simpb 997 . . . . . . . . 9  |-  ( ( f  e.  ( om 
X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  ->  ( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
) )
6160adantr 276 . . . . . . . 8  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
f  e.  ( om 
X.  N. )  /\  h  e.  ( om  X.  N. ) ) )
62 simplll 533 . . . . . . . . . 10  |-  ( ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  ->  f  =  <. z ,  w >. )
63 simprlr 538 . . . . . . . . . 10  |-  ( ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  ->  h  =  <. s ,  t >.
)
6462, 63jca 306 . . . . . . . . 9  |-  ( ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  ->  ( f  =  <. z ,  w >.  /\  h  =  <. s ,  t >. )
)
6564adantl 277 . . . . . . . 8  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
f  =  <. z ,  w >.  /\  h  =  <. s ,  t
>. ) )
66 oveq1 5903 . . . . . . . . . . . . . . . 16  |-  ( v  =  (/)  ->  ( v  .o  t )  =  ( (/)  .o  t
) )
6763adantl 277 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  h  =  <. s ,  t
>. )
68 simpl3 1004 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  h  e.  ( om  X.  N. ) )
6967, 68eqeltrrd 2267 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  <. s ,  t >.  e.  ( om  X.  N. )
)
70 opelxp 4674 . . . . . . . . . . . . . . . . . . . . 21  |-  ( <.
s ,  t >.  e.  ( om  X.  N. ) 
<->  ( s  e.  om  /\  t  e.  N. )
)
7169, 70sylib 122 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
s  e.  om  /\  t  e.  N. )
)
7271simprd 114 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  t  e.  N. )
73 pinn 7338 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  N.  ->  t  e.  om )
7472, 73syl 14 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  t  e.  om )
75 nnm0r 6504 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  om  ->  ( (/) 
.o  t )  =  (/) )
7674, 75syl 14 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  ( (/) 
.o  t )  =  (/) )
7776eqeq2d 2201 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( v  .o  t
)  =  ( (/)  .o  t )  <->  ( v  .o  t )  =  (/) ) )
7866, 77imbitrid 154 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  (
v  .o  t )  =  (/) ) )
79 simprr 531 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  ->  ( a  .o  t )  =  ( b  .o  s ) )
80 eqtr2 2208 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g  =  <. v ,  u >.  /\  g  =  <. a ,  b
>. )  ->  <. v ,  u >.  =  <. a ,  b >. )
81 vex 2755 . . . . . . . . . . . . . . . . . . . . . . 23  |-  v  e. 
_V
82 vex 2755 . . . . . . . . . . . . . . . . . . . . . . 23  |-  u  e. 
_V
8381, 82opth 4255 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( <.
v ,  u >.  = 
<. a ,  b >.  <->  ( v  =  a  /\  u  =  b )
)
8480, 83sylib 122 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g  =  <. v ,  u >.  /\  g  =  <. a ,  b
>. )  ->  ( v  =  a  /\  u  =  b ) )
85 oveq1 5903 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  =  a  ->  (
v  .o  t )  =  ( a  .o  t ) )
86 oveq1 5903 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  b  ->  (
u  .o  s )  =  ( b  .o  s ) )
8785, 86eqeqan12d 2205 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( v  =  a  /\  u  =  b )  ->  ( ( v  .o  t )  =  ( u  .o  s )  <-> 
( a  .o  t
)  =  ( b  .o  s ) ) )
8884, 87syl 14 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  =  <. v ,  u >.  /\  g  =  <. a ,  b
>. )  ->  ( ( v  .o  t )  =  ( u  .o  s )  <->  ( a  .o  t )  =  ( b  .o  s ) ) )
8988ad2ant2lr 510 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )
)  ->  ( (
v  .o  t )  =  ( u  .o  s )  <->  ( a  .o  t )  =  ( b  .o  s ) ) )
9089ad2ant2r 509 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  ->  ( (
v  .o  t )  =  ( u  .o  s )  <->  ( a  .o  t )  =  ( b  .o  s ) ) )
9179, 90mpbird 167 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  ->  ( v  .o  t )  =  ( u  .o  s ) )
9291eqeq1d 2198 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  ->  ( (
v  .o  t )  =  (/)  <->  ( u  .o  s )  =  (/) ) )
9392adantl 277 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( v  .o  t
)  =  (/)  <->  ( u  .o  s )  =  (/) ) )
9478, 93sylibd 149 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  (
u  .o  s )  =  (/) ) )
95 simpllr 534 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  ->  g  =  <. v ,  u >. )
9695adantl 277 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  g  =  <. v ,  u >. )
97 simpl2 1003 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  g  e.  ( om  X.  N. ) )
9896, 97eqeltrrd 2267 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  <. v ,  u >.  e.  ( om  X.  N. ) )
99 opelxp 4674 . . . . . . . . . . . . . . . . . 18  |-  ( <.
v ,  u >.  e.  ( om  X.  N. ) 
<->  ( v  e.  om  /\  u  e.  N. )
)
10098, 99sylib 122 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  e.  om  /\  u  e.  N. )
)
101100simprd 114 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  u  e.  N. )
102 pinn 7338 . . . . . . . . . . . . . . . 16  |-  ( u  e.  N.  ->  u  e.  om )
103101, 102syl 14 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  u  e.  om )
10471simpld 112 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  s  e.  om )
105 nnm00 6555 . . . . . . . . . . . . . . 15  |-  ( ( u  e.  om  /\  s  e.  om )  ->  ( ( u  .o  s )  =  (/)  <->  (
u  =  (/)  \/  s  =  (/) ) ) )
106103, 104, 105syl2anc 411 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( u  .o  s
)  =  (/)  <->  ( u  =  (/)  \/  s  =  (/) ) ) )
10794, 106sylibd 149 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  (
u  =  (/)  \/  s  =  (/) ) ) )
108 elni2 7343 . . . . . . . . . . . . . . . 16  |-  ( u  e.  N.  <->  ( u  e.  om  /\  (/)  e.  u
) )
109108simprbi 275 . . . . . . . . . . . . . . 15  |-  ( u  e.  N.  ->  (/)  e.  u
)
110101, 109syl 14 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (/)  e.  u
)
111 n0i 3443 . . . . . . . . . . . . . 14  |-  ( (/)  e.  u  ->  -.  u  =  (/) )
112 biorf 745 . . . . . . . . . . . . . 14  |-  ( -.  u  =  (/)  ->  (
s  =  (/)  <->  ( u  =  (/)  \/  s  =  (/) ) ) )
113110, 111, 1123syl 17 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
s  =  (/)  <->  ( u  =  (/)  \/  s  =  (/) ) ) )
114107, 113sylibrd 169 . . . . . . . . . . . 12  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  s  =  (/) ) )
11562adantl 277 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  f  =  <. z ,  w >. )
116 simpl1 1002 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  f  e.  ( om  X.  N. ) )
117115, 116eqeltrrd 2267 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  <. z ,  w >.  e.  ( om  X.  N. ) )
118 opelxp 4674 . . . . . . . . . . . . . . . . 17  |-  ( <.
z ,  w >.  e.  ( om  X.  N. ) 
<->  ( z  e.  om  /\  w  e.  N. )
)
119117, 118sylib 122 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
z  e.  om  /\  w  e.  N. )
)
120119simprd 114 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  w  e.  N. )
121 pinn 7338 . . . . . . . . . . . . . . 15  |-  ( w  e.  N.  ->  w  e.  om )
122120, 121syl 14 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  w  e.  om )
123 nnm0 6500 . . . . . . . . . . . . . 14  |-  ( w  e.  om  ->  (
w  .o  (/) )  =  (/) )
124122, 123syl 14 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
w  .o  (/) )  =  (/) )
125 oveq2 5904 . . . . . . . . . . . . . 14  |-  ( s  =  (/)  ->  ( w  .o  s )  =  ( w  .o  (/) ) )
126125eqeq1d 2198 . . . . . . . . . . . . 13  |-  ( s  =  (/)  ->  ( ( w  .o  s )  =  (/)  <->  ( w  .o  (/) )  =  (/) ) )
127124, 126syl5ibrcom 157 . . . . . . . . . . . 12  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
s  =  (/)  ->  (
w  .o  s )  =  (/) ) )
128114, 127syld 45 . . . . . . . . . . 11  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  (
w  .o  s )  =  (/) ) )
129 oveq2 5904 . . . . . . . . . . . . . . . 16  |-  ( v  =  (/)  ->  ( w  .o  v )  =  ( w  .o  (/) ) )
130124eqeq2d 2201 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( w  .o  v
)  =  ( w  .o  (/) )  <->  ( w  .o  v )  =  (/) ) )
131129, 130imbitrid 154 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  (
w  .o  v )  =  (/) ) )
132 simprlr 538 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
z  .o  u )  =  ( w  .o  v ) )
133132eqeq1d 2198 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( z  .o  u
)  =  (/)  <->  ( w  .o  v )  =  (/) ) )
134131, 133sylibrd 169 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  (
z  .o  u )  =  (/) ) )
135119simpld 112 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  z  e.  om )
136 nnm00 6555 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  om  /\  u  e.  om )  ->  ( ( z  .o  u )  =  (/)  <->  (
z  =  (/)  \/  u  =  (/) ) ) )
137135, 103, 136syl2anc 411 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( z  .o  u
)  =  (/)  <->  ( z  =  (/)  \/  u  =  (/) ) ) )
138134, 137sylibd 149 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  (
z  =  (/)  \/  u  =  (/) ) ) )
139 biorf 745 . . . . . . . . . . . . . . 15  |-  ( -.  u  =  (/)  ->  (
z  =  (/)  <->  ( u  =  (/)  \/  z  =  (/) ) ) )
140 orcom 729 . . . . . . . . . . . . . . 15  |-  ( ( u  =  (/)  \/  z  =  (/) )  <->  ( z  =  (/)  \/  u  =  (/) ) )
141139, 140bitrdi 196 . . . . . . . . . . . . . 14  |-  ( -.  u  =  (/)  ->  (
z  =  (/)  <->  ( z  =  (/)  \/  u  =  (/) ) ) )
142110, 111, 1413syl 17 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
z  =  (/)  <->  ( z  =  (/)  \/  u  =  (/) ) ) )
143138, 142sylibrd 169 . . . . . . . . . . . 12  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  z  =  (/) ) )
144 oveq1 5903 . . . . . . . . . . . . . 14  |-  ( z  =  (/)  ->  ( z  .o  t )  =  ( (/)  .o  t
) )
145144eqeq1d 2198 . . . . . . . . . . . . 13  |-  ( z  =  (/)  ->  ( ( z  .o  t )  =  (/)  <->  ( (/)  .o  t
)  =  (/) ) )
14676, 145syl5ibrcom 157 . . . . . . . . . . . 12  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
z  =  (/)  ->  (
z  .o  t )  =  (/) ) )
147143, 146syld 45 . . . . . . . . . . 11  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  (
z  .o  t )  =  (/) ) )
148128, 147jcad 307 . . . . . . . . . 10  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  (
( w  .o  s
)  =  (/)  /\  (
z  .o  t )  =  (/) ) ) )
149 eqtr3 2209 . . . . . . . . . . 11  |-  ( ( ( w  .o  s
)  =  (/)  /\  (
z  .o  t )  =  (/) )  ->  (
w  .o  s )  =  ( z  .o  t ) )
150149eqcomd 2195 . . . . . . . . . 10  |-  ( ( ( w  .o  s
)  =  (/)  /\  (
z  .o  t )  =  (/) )  ->  (
z  .o  t )  =  ( w  .o  s ) )
151148, 150syl6 33 . . . . . . . . 9  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  ->  (
z  .o  t )  =  ( w  .o  s ) ) )
152 simplr 528 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  ->  ( z  .o  u )  =  ( w  .o  v ) )
15391, 152oveq12d 5914 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( f  = 
<. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  (
z  .o  u )  =  ( w  .o  v ) )  /\  ( ( g  = 
<. a ,  b >.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) )  ->  ( (
v  .o  t )  .o  ( z  .o  u ) )  =  ( ( u  .o  s )  .o  (
w  .o  v ) ) )
154153adantl 277 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( v  .o  t
)  .o  ( z  .o  u ) )  =  ( ( u  .o  s )  .o  ( w  .o  v
) ) )
155100simpld 112 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  v  e.  om )
156 nnmcl 6506 . . . . . . . . . . . . . . . . 17  |-  ( ( v  e.  om  /\  t  e.  om )  ->  ( v  .o  t
)  e.  om )
157155, 74, 156syl2anc 411 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  .o  t )  e.  om )
158 nnmcom 6514 . . . . . . . . . . . . . . . . 17  |-  ( ( c  e.  om  /\  d  e.  om )  ->  ( c  .o  d
)  =  ( d  .o  c ) )
159158adantl 277 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  /\  ( c  e.  om  /\  d  e.  om ) )  -> 
( c  .o  d
)  =  ( d  .o  c ) )
160 nnmass 6512 . . . . . . . . . . . . . . . . 17  |-  ( ( c  e.  om  /\  d  e.  om  /\  e  e.  om )  ->  (
( c  .o  d
)  .o  e )  =  ( c  .o  ( d  .o  e
) ) )
161160adantl 277 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  /\  ( c  e.  om  /\  d  e.  om  /\  e  e. 
om ) )  -> 
( ( c  .o  d )  .o  e
)  =  ( c  .o  ( d  .o  e ) ) )
162157, 135, 103, 159, 161caov13d 6080 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( v  .o  t
)  .o  ( z  .o  u ) )  =  ( u  .o  ( z  .o  (
v  .o  t ) ) ) )
163 nnmcl 6506 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e.  om  /\  v  e.  om )  ->  ( w  .o  v
)  e.  om )
164122, 155, 163syl2anc 411 . . . . . . . . . . . . . . . 16  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
w  .o  v )  e.  om )
165161, 103, 104, 164caovassd 6056 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( u  .o  s
)  .o  ( w  .o  v ) )  =  ( u  .o  ( s  .o  (
w  .o  v ) ) ) )
166154, 162, 1653eqtr3d 2230 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
u  .o  ( z  .o  ( v  .o  t ) ) )  =  ( u  .o  ( s  .o  (
w  .o  v ) ) ) )
167 nnmcl 6506 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  om  /\  ( v  .o  t
)  e.  om )  ->  ( z  .o  (
v  .o  t ) )  e.  om )
168135, 157, 167syl2anc 411 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
z  .o  ( v  .o  t ) )  e.  om )
169 nnmcl 6506 . . . . . . . . . . . . . . . 16  |-  ( ( s  e.  om  /\  ( w  .o  v
)  e.  om )  ->  ( s  .o  (
w  .o  v ) )  e.  om )
170104, 164, 169syl2anc 411 . . . . . . . . . . . . . . 15  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
s  .o  ( w  .o  v ) )  e.  om )
171 nnmcan 6544 . . . . . . . . . . . . . . 15  |-  ( ( ( u  e.  om  /\  ( z  .o  (
v  .o  t ) )  e.  om  /\  ( s  .o  (
w  .o  v ) )  e.  om )  /\  (/)  e.  u )  ->  ( ( u  .o  ( z  .o  ( v  .o  t
) ) )  =  ( u  .o  (
s  .o  ( w  .o  v ) ) )  <->  ( z  .o  ( v  .o  t
) )  =  ( s  .o  ( w  .o  v ) ) ) )
172103, 168, 170, 110, 171syl31anc 1252 . . . . . . . . . . . . . 14  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( u  .o  (
z  .o  ( v  .o  t ) ) )  =  ( u  .o  ( s  .o  ( w  .o  v
) ) )  <->  ( z  .o  ( v  .o  t
) )  =  ( s  .o  ( w  .o  v ) ) ) )
173166, 172mpbid 147 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
z  .o  ( v  .o  t ) )  =  ( s  .o  ( w  .o  v
) ) )
174135, 155, 74, 159, 161caov12d 6078 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
z  .o  ( v  .o  t ) )  =  ( v  .o  ( z  .o  t
) ) )
175104, 122, 155, 159, 161caov13d 6080 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
s  .o  ( w  .o  v ) )  =  ( v  .o  ( w  .o  s
) ) )
176173, 174, 1753eqtr3d 2230 . . . . . . . . . . . 12  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  .o  ( z  .o  t ) )  =  ( v  .o  ( w  .o  s
) ) )
177176adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  /\  (/)  e.  v )  ->  ( v  .o  ( z  .o  t
) )  =  ( v  .o  ( w  .o  s ) ) )
178 nnmcl 6506 . . . . . . . . . . . . . 14  |-  ( ( z  e.  om  /\  t  e.  om )  ->  ( z  .o  t
)  e.  om )
179135, 74, 178syl2anc 411 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
z  .o  t )  e.  om )
180 nnmcl 6506 . . . . . . . . . . . . . 14  |-  ( ( w  e.  om  /\  s  e.  om )  ->  ( w  .o  s
)  e.  om )
181122, 104, 180syl2anc 411 . . . . . . . . . . . . 13  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
w  .o  s )  e.  om )
182155, 179, 1813jca 1179 . . . . . . . . . . . 12  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  e.  om  /\  ( z  .o  t
)  e.  om  /\  ( w  .o  s
)  e.  om )
)
183 nnmcan 6544 . . . . . . . . . . . 12  |-  ( ( ( v  e.  om  /\  ( z  .o  t
)  e.  om  /\  ( w  .o  s
)  e.  om )  /\  (/)  e.  v )  ->  ( ( v  .o  ( z  .o  t ) )  =  ( v  .o  (
w  .o  s ) )  <->  ( z  .o  t )  =  ( w  .o  s ) ) )
184182, 183sylan 283 . . . . . . . . . . 11  |-  ( ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  /\  (/)  e.  v )  ->  ( (
v  .o  ( z  .o  t ) )  =  ( v  .o  ( w  .o  s
) )  <->  ( z  .o  t )  =  ( w  .o  s ) ) )
185177, 184mpbid 147 . . . . . . . . . 10  |-  ( ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  /\  (/)  e.  v )  ->  ( z  .o  t )  =  ( w  .o  s ) )
186185ex 115 . . . . . . . . 9  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  ( (/) 
e.  v  ->  (
z  .o  t )  =  ( w  .o  s ) ) )
187 0elnn 4636 . . . . . . . . . 10  |-  ( v  e.  om  ->  (
v  =  (/)  \/  (/)  e.  v ) )
188155, 187syl 14 . . . . . . . . 9  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
v  =  (/)  \/  (/)  e.  v ) )
189151, 186, 188mpjaod 719 . . . . . . . 8  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
z  .o  t )  =  ( w  .o  s ) )
19061, 65, 189jca32 310 . . . . . . 7  |-  ( ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  (
( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( f  =  <. z ,  w >.  /\  h  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) ) )
1911902eximi 1612 . . . . . 6  |-  ( E. s E. t ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  E. s E. t ( ( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  (
( f  =  <. z ,  w >.  /\  h  =  <. s ,  t
>. )  /\  (
z  .o  t )  =  ( w  .o  s ) ) ) )
192191exlimivv 1908 . . . . 5  |-  ( E. a E. b E. s E. t ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  ( ( ( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  /\  ( ( g  =  <. a ,  b
>.  /\  h  =  <. s ,  t >. )  /\  ( a  .o  t
)  =  ( b  .o  s ) ) ) )  ->  E. s E. t ( ( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  (
( f  =  <. z ,  w >.  /\  h  =  <. s ,  t
>. )  /\  (
z  .o  t )  =  ( w  .o  s ) ) ) )
193192exlimivv 1908 . . . 4  |-  ( E. v E. u E. a E. b E. s E. t ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  ( (
( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  ->  E. s E. t ( ( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  (
( f  =  <. z ,  w >.  /\  h  =  <. s ,  t
>. )  /\  (
z  .o  t )  =  ( w  .o  s ) ) ) )
1941932eximi 1612 . . 3  |-  ( E. z E. w E. v E. u E. a E. b E. s E. t ( ( f  e.  ( om  X.  N. )  /\  g  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  ( (
( f  =  <. z ,  w >.  /\  g  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) )  /\  (
( g  =  <. a ,  b >.  /\  h  =  <. s ,  t
>. )  /\  (
a  .o  t )  =  ( b  .o  s ) ) ) )  ->  E. z E. w E. s E. t ( ( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  (
( f  =  <. z ,  w >.  /\  h  =  <. s ,  t
>. )  /\  (
z  .o  t )  =  ( w  .o  s ) ) ) )
19559, 194syl 14 . 2  |-  ( ( f ~Q0  g  /\  g ~Q0  h )  ->  E. z E. w E. s E. t ( ( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  (
( f  =  <. z ,  w >.  /\  h  =  <. s ,  t
>. )  /\  (
z  .o  t )  =  ( w  .o  s ) ) ) )
196 19.42vvvv 1925 . . 3  |-  ( E. z E. w E. s E. t ( ( f  e.  ( om 
X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  (
( f  =  <. z ,  w >.  /\  h  =  <. s ,  t
>. )  /\  (
z  .o  t )  =  ( w  .o  s ) ) )  <-> 
( ( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. )
)  /\  E. z E. w E. s E. t ( ( f  =  <. z ,  w >.  /\  h  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) ) )
1975anbi1d 465 . . . . . . 7  |-  ( x  =  f  ->  (
( x  =  <. z ,  w >.  /\  y  =  <. s ,  t
>. )  <->  ( f  = 
<. z ,  w >.  /\  y  =  <. s ,  t >. )
) )
198197anbi1d 465 . . . . . 6  |-  ( x  =  f  ->  (
( ( x  = 
<. z ,  w >.  /\  y  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) )  <-> 
( ( f  = 
<. z ,  w >.  /\  y  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) ) )
1991984exbidv 1881 . . . . 5  |-  ( x  =  f  ->  ( E. z E. w E. s E. t ( ( x  =  <. z ,  w >.  /\  y  =  <. s ,  t
>. )  /\  (
z  .o  t )  =  ( w  .o  s ) )  <->  E. z E. w E. s E. t ( ( f  =  <. z ,  w >.  /\  y  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) ) )
2004, 199anbi12d 473 . . . 4  |-  ( x  =  f  ->  (
( ( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. )
)  /\  E. z E. w E. s E. t ( ( x  =  <. z ,  w >.  /\  y  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) )  <->  ( ( f  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  E. z E. w E. s E. t ( ( f  =  <. z ,  w >.  /\  y  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) ) ) )
20127anbi2d 464 . . . . 5  |-  ( y  =  h  ->  (
( f  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  <-> 
( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) ) ) )
20229anbi2d 464 . . . . . . 7  |-  ( y  =  h  ->  (
( f  =  <. z ,  w >.  /\  y  =  <. s ,  t
>. )  <->  ( f  = 
<. z ,  w >.  /\  h  =  <. s ,  t >. )
) )
203202anbi1d 465 . . . . . 6  |-  ( y  =  h  ->  (
( ( f  = 
<. z ,  w >.  /\  y  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) )  <-> 
( ( f  = 
<. z ,  w >.  /\  h  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) ) )
2042034exbidv 1881 . . . . 5  |-  ( y  =  h  ->  ( E. z E. w E. s E. t ( ( f  =  <. z ,  w >.  /\  y  =  <. s ,  t
>. )  /\  (
z  .o  t )  =  ( w  .o  s ) )  <->  E. z E. w E. s E. t ( ( f  =  <. z ,  w >.  /\  h  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) ) )
205201, 204anbi12d 473 . . . 4  |-  ( y  =  h  ->  (
( ( f  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. )
)  /\  E. z E. w E. s E. t ( ( f  =  <. z ,  w >.  /\  y  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) )  <->  ( ( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. z E. w E. s E. t ( ( f  =  <. z ,  w >.  /\  h  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) ) ) )
206 df-enq0 7453 . . . 4  |- ~Q0  =  { <. x ,  y >.  |  ( ( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  E. z E. w E. s E. t ( ( x  =  <. z ,  w >.  /\  y  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) ) }
2071, 19, 200, 205, 206brab 4290 . . 3  |-  ( f ~Q0  h  <->  ( ( f  e.  ( om  X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  E. z E. w E. s E. t ( ( f  =  <. z ,  w >.  /\  h  =  <. s ,  t >. )  /\  ( z  .o  t
)  =  ( w  .o  s ) ) ) )
208196, 207bitr4i 187 . 2  |-  ( E. z E. w E. s E. t ( ( f  e.  ( om 
X.  N. )  /\  h  e.  ( om  X.  N. ) )  /\  (
( f  =  <. z ,  w >.  /\  h  =  <. s ,  t
>. )  /\  (
z  .o  t )  =  ( w  .o  s ) ) )  <-> 
f ~Q0  h )
209195, 208sylib 122 1  |-  ( ( f ~Q0  g  /\  g ~Q0  h )  ->  f ~Q0  h )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 709    /\ w3a 980    = wceq 1364   E.wex 1503    e. wcel 2160   (/)c0 3437   <.cop 3610   class class class wbr 4018   omcom 4607    X. cxp 4642  (class class class)co 5896    .o comu 6439   N.cnpi 7301   ~Q0 ceq0 7315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-iinf 4605
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4311  df-iord 4384  df-on 4386  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-ov 5899  df-oprab 5900  df-mpo 5901  df-1st 6165  df-2nd 6166  df-recs 6330  df-irdg 6395  df-oadd 6445  df-omul 6446  df-ni 7333  df-enq0 7453
This theorem is referenced by:  enq0er  7464
  Copyright terms: Public domain W3C validator