Metamath Proof Explorer


Theorem sltres

Description: If the restrictions of two surreals to a given ordinal obey surreal less than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011)

Ref Expression
Assertion sltres
|- ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  A 

Proof

Step Hyp Ref Expression
1 noreson
 |-  ( ( A e. No /\ X e. On ) -> ( A |` X ) e. No )
2 1 3adant2
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( A |` X ) e. No )
3 noreson
 |-  ( ( B e. No /\ X e. On ) -> ( B |` X ) e. No )
4 3 3adant1
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( B |` X ) e. No )
5 sltintdifex
 |-  ( ( ( A |` X ) e. No /\ ( B |` X ) e. No ) -> ( ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. _V ) )
6 onintrab
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. _V <-> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On )
7 5 6 syl6ib
 |-  ( ( ( A |` X ) e. No /\ ( B |` X ) e. No ) -> ( ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On ) )
8 2 4 7 syl2anc
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On ) )
9 8 imp
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On )
10 simpl3
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  X e. On )
11 sltval2
 |-  ( ( ( A |` X ) e. No /\ ( B |` X ) e. No ) -> ( ( A |` X )  ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) )
12 2 4 11 syl2anc
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) )
13 fvex
 |-  ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. _V
14 fvex
 |-  ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. _V
15 13 14 brtp
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) <-> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) )
16 1n0
 |-  1o =/= (/)
17 16 neii
 |-  -. 1o = (/)
18 eqeq1
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) <-> 1o = (/) ) )
19 17 18 mtbiri
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> -. ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
20 ndmfv
 |-  ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
21 19 20 nsyl2
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
22 21 adantr
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
23 22 orcd
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
24 21 adantr
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
25 24 orcd
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
26 2on
 |-  2o e. On
27 26 elexi
 |-  2o e. _V
28 27 prid2
 |-  2o e. { 1o , 2o }
29 28 nosgnn0i
 |-  (/) =/= 2o
30 29 neii
 |-  -. (/) = 2o
31 eqeq1
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) <-> 2o = (/) ) )
32 eqcom
 |-  ( 2o = (/) <-> (/) = 2o )
33 31 32 bitrdi
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) <-> (/) = 2o ) )
34 30 33 mtbiri
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> -. ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
35 ndmfv
 |-  ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
36 34 35 nsyl2
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) )
37 36 adantl
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) )
38 37 olcd
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
39 23 25 38 3jaoi
 |-  ( ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
40 15 39 sylbi
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
41 12 40 syl6bi
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) ) )
42 41 imp
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
43 dmres
 |-  dom ( A |` X ) = ( X i^i dom A )
44 43 elin2
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) <-> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X /\ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A ) )
45 44 simplbi
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
46 dmres
 |-  dom ( B |` X ) = ( X i^i dom B )
47 46 elin2
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) <-> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X /\ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom B ) )
48 47 simplbi
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
49 45 48 jaoi
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
50 42 49 syl
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
51 onelss
 |-  ( X e. On -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } C_ X ) )
52 10 50 51 sylc
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } C_ X )
53 52 sselda
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  y e. X )
54 onelon
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On /\ y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) -> y e. On )
55 9 54 sylan
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  y e. On )
56 intss1
 |-  ( y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } C_ y )
57 ontri1
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On /\ y e. On ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } C_ y <-> -. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
58 56 57 syl5ib
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On /\ y e. On ) -> ( y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> -. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
59 58 con2d
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On /\ y e. On ) -> ( y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> -. y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
60 9 59 sylan
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> -. y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
61 60 impancom
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( y e. On -> -. y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
62 55 61 mpd
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  -. y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } )
63 fveq2
 |-  ( a = y -> ( ( A |` X ) ` a ) = ( ( A |` X ) ` y ) )
64 fveq2
 |-  ( a = y -> ( ( B |` X ) ` a ) = ( ( B |` X ) ` y ) )
65 63 64 neeq12d
 |-  ( a = y -> ( ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) <-> ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) ) )
66 65 elrab
 |-  ( y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } <-> ( y e. On /\ ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) ) )
67 66 simplbi2
 |-  ( y e. On -> ( ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) -> y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
68 67 con3d
 |-  ( y e. On -> ( -. y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> -. ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) ) )
69 55 62 68 sylc
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  -. ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) )
70 df-ne
 |-  ( ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) <-> -. ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) )
71 70 con2bii
 |-  ( ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) <-> -. ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) )
72 69 71 sylibr
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) )
73 fvres
 |-  ( y e. X -> ( ( A |` X ) ` y ) = ( A ` y ) )
74 fvres
 |-  ( y e. X -> ( ( B |` X ) ` y ) = ( B ` y ) )
75 73 74 eqeq12d
 |-  ( y e. X -> ( ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) <-> ( A ` y ) = ( B ` y ) ) )
76 75 biimpd
 |-  ( y e. X -> ( ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) -> ( A ` y ) = ( B ` y ) ) )
77 53 72 76 sylc
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( A ` y ) = ( B ` y ) )
78 77 ralrimiva
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  A. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ( A ` y ) = ( B ` y ) )
79 fvresval
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) \/ ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
80 79 ori
 |-  ( -. ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
81 19 80 nsyl2
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
82 81 eqcomd
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
83 eqeq2
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) <-> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o ) )
84 82 83 mpbid
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o )
85 84 adantr
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o )
86 85 a1i
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o ) )
87 21 ad2antrl
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
88 87 45 syl
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
89 nofun
 |-  ( ( B |` X ) e. No -> Fun ( B |` X ) )
90 fvelrn
 |-  ( ( Fun ( B |` X ) /\ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( B |` X ) )
91 90 ex
 |-  ( Fun ( B |` X ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( B |` X ) ) )
92 89 91 syl
 |-  ( ( B |` X ) e. No -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( B |` X ) ) )
93 norn
 |-  ( ( B |` X ) e. No -> ran ( B |` X ) C_ { 1o , 2o } )
94 93 sseld
 |-  ( ( B |` X ) e. No -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( B |` X ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } ) )
95 92 94 syld
 |-  ( ( B |` X ) e. No -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } ) )
96 nosgnn0
 |-  -. (/) e. { 1o , 2o }
97 eleq1
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } <-> (/) e. { 1o , 2o } ) )
98 96 97 mtbiri
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } )
99 95 98 nsyli
 |-  ( ( B |` X ) e. No -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
100 4 99 syl
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
101 100 imp
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) )
102 101 adantrl
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) )
103 47 simplbi2
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom B -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
104 103 con3d
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X -> ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom B ) )
105 88 102 104 sylc
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom B )
106 ndmfv
 |-  ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom B -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
107 105 106 syl
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
108 107 ex
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) )
109 86 108 jcad
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) )
110 fvresval
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) \/ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
111 110 ori
 |-  ( -. ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
112 34 111 nsyl2
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
113 112 eqcomd
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
114 eqeq2
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) <-> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) )
115 113 114 mpbid
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o )
116 84 115 anim12i
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) )
117 116 a1i
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) )
118 36 ad2antll
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) )
119 118 48 syl
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
120 nofun
 |-  ( ( A |` X ) e. No -> Fun ( A |` X ) )
121 fvelrn
 |-  ( ( Fun ( A |` X ) /\ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( A |` X ) )
122 121 ex
 |-  ( Fun ( A |` X ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( A |` X ) ) )
123 120 122 syl
 |-  ( ( A |` X ) e. No -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( A |` X ) ) )
124 norn
 |-  ( ( A |` X ) e. No -> ran ( A |` X ) C_ { 1o , 2o } )
125 124 sseld
 |-  ( ( A |` X ) e. No -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( A |` X ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } ) )
126 123 125 syld
 |-  ( ( A |` X ) e. No -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } ) )
127 eleq1
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } <-> (/) e. { 1o , 2o } ) )
128 96 127 mtbiri
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } )
129 126 128 nsyli
 |-  ( ( A |` X ) e. No -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) ) )
130 2 129 syl
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) ) )
131 130 imp
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
132 131 adantrr
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
133 44 simplbi2
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) ) )
134 133 con3d
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X -> ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A ) )
135 119 132 134 sylc
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A )
136 135 ex
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A ) )
137 ndmfv
 |-  ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
138 136 137 syl6
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) )
139 115 adantl
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o )
140 139 a1i
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) )
141 138 140 jcad
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) )
142 109 117 141 3orim123d
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> ( ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) ) )
143 fvex
 |-  ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. _V
144 fvex
 |-  ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. _V
145 143 144 brtp
 |-  ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) <-> ( ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) )
146 142 15 145 3imtr4g
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) )
147 12 146 sylbid
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) )
148 147 imp
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
149 raleq
 |-  ( x = |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> ( A. y e. x ( A ` y ) = ( B ` y ) <-> A. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ( A ` y ) = ( B ` y ) ) )
150 fveq2
 |-  ( x = |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> ( A ` x ) = ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
151 fveq2
 |-  ( x = |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> ( B ` x ) = ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
152 150 151 breq12d
 |-  ( x = |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) )
153 149 152 anbi12d
 |-  ( x = |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> ( ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> ( A. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ( A ` y ) = ( B ` y ) /\ ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) ) )
154 153 rspcev
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On /\ ( A. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ( A ` y ) = ( B ` y ) /\ ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) ) -> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
155 9 78 148 154 syl12anc
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
156 sltval
 |-  ( ( A e. No /\ B e. No ) -> ( A  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
157 156 3adant3
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( A  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
158 157 adantr
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( A  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
159 155 158 mpbird
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  A 
160 159 ex
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  A