Metamath Proof Explorer

Theorem nolt02o

Description: Given A less-than B , equal to B up to X , and undefined at X , then B ( X ) = 2o . (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nolt02o 
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( B ` X ) = 2o )

Proof

Step Hyp Ref Expression
1 simp11 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A e. No )
2 sltso 
 |-
3 sonr 
 |-  ( (  -. A
4 2 3 mpan 
 |-  ( A e. No -> -. A
5 1 4 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. A
6 simp2r 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A
7 breq2 
 |-  ( A = B -> ( A  A
8 6 7 syl5ibrcom 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A = B -> A
9 5 8 mtod 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. A = B )
10 simpl2l 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A |` X ) = ( B |` X ) )
11 simpl11 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A e. No )
12 nofun 
 |-  ( A e. No -> Fun A )
13 funrel 
 |-  ( Fun A -> Rel A )
14 11 12 13 3syl 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  Rel A )
15 simpl13 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  X e. On )
16 simpl3 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A ` X ) = (/) )
17 nolt02olem 
 |-  ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> dom A C_ X )
18 11 15 16 17 syl3anc 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  dom A C_ X )
19 relssres 
 |-  ( ( Rel A /\ dom A C_ X ) -> ( A |` X ) = A )
20 14 18 19 syl2anc 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A |` X ) = A )
21 simpl12 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  B e. No )
22 nofun 
 |-  ( B e. No -> Fun B )
23 funrel 
 |-  ( Fun B -> Rel B )
24 21 22 23 3syl 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  Rel B )
25 simpr 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( B ` X ) = (/) )
26 nolt02olem 
 |-  ( ( B e. No /\ X e. On /\ ( B ` X ) = (/) ) -> dom B C_ X )
27 21 15 25 26 syl3anc 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  dom B C_ X )
28 relssres 
 |-  ( ( Rel B /\ dom B C_ X ) -> ( B |` X ) = B )
29 24 27 28 syl2anc 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( B |` X ) = B )
30 10 20 29 3eqtr3d 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A = B )
31 9 30 mtand 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. ( B ` X ) = (/) )
32 simp12 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  B e. No )
33 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 ) ) ) )
34 1 32 33 syl2anc 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
35 6 34 mpbid 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
36 df-an 
 |-  ( ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> -. ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
37 36 rexbii 
 |-  ( E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> E. x e. On -. ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
38 rexnal 
 |-  ( E. x e. On -. ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> -. A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
39 37 38 bitri 
 |-  ( E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> -. A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
40 35 39 sylib 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
41 1oex 
 |-  1o e. _V
42 41 prid1 
 |-  1o e. { 1o , 2o }
43 42 nosgnn0i 
 |-  (/) =/= 1o
44 43 neii 
 |-  -. (/) = 1o
45 simpll3 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A ` X ) = (/) )
46 simplr 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( B ` X ) = 1o )
47 eqeq1 
 |-  ( ( A ` X ) = ( B ` X ) -> ( ( A ` X ) = (/) <-> ( B ` X ) = (/) ) )
48 47 anbi1d 
 |-  ( ( A ` X ) = ( B ` X ) -> ( ( ( A ` X ) = (/) /\ ( B ` X ) = 1o ) <-> ( ( B ` X ) = (/) /\ ( B ` X ) = 1o ) ) )
49 eqtr2 
 |-  ( ( ( B ` X ) = (/) /\ ( B ` X ) = 1o ) -> (/) = 1o )
50 48 49 biimtrdi 
 |-  ( ( A ` X ) = ( B ` X ) -> ( ( ( A ` X ) = (/) /\ ( B ` X ) = 1o ) -> (/) = 1o ) )
51 50 com12 
 |-  ( ( ( A ` X ) = (/) /\ ( B ` X ) = 1o ) -> ( ( A ` X ) = ( B ` X ) -> (/) = 1o ) )
52 45 46 51 syl2anc 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( A ` X ) = ( B ` X ) -> (/) = 1o ) )
53 44 52 mtoi 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. ( A ` X ) = ( B ` X ) )
54 simpr 
 |-  ( ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  X e. x )
55 simplrr 
 |-  ( ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A. y e. x ( A ` y ) = ( B ` y ) )
56 fveq2 
 |-  ( y = X -> ( A ` y ) = ( A ` X ) )
57 fveq2 
 |-  ( y = X -> ( B ` y ) = ( B ` X ) )
58 56 57 eqeq12d 
 |-  ( y = X -> ( ( A ` y ) = ( B ` y ) <-> ( A ` X ) = ( B ` X ) ) )
59 58 rspcv 
 |-  ( X e. x -> ( A. y e. x ( A ` y ) = ( B ` y ) -> ( A ` X ) = ( B ` X ) ) )
60 54 55 59 sylc 
 |-  ( ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A ` X ) = ( B ` X ) )
61 53 60 mtand 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. X e. x )
62 simprl 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  x e. On )
63 simpl13 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  X e. On )
64 63 adantr 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  X e. On )
65 ontri1 
 |-  ( ( x e. On /\ X e. On ) -> ( x C_ X <-> -. X e. x ) )
66 62 64 65 syl2anc 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( x C_ X <-> -. X e. x ) )
67 61 66 mpbird 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  x C_ X )
68 onsseleq 
 |-  ( ( x e. On /\ X e. On ) -> ( x C_ X <-> ( x e. X \/ x = X ) ) )
69 62 64 68 syl2anc 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( x C_ X <-> ( x e. X \/ x = X ) ) )
70 eqtr2 
 |-  ( ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 1o ) -> (/) = 1o )
71 70 ancoms 
 |-  ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) -> (/) = 1o )
72 44 71 mto 
 |-  -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) )
73 df-1o 
 |-  1o = suc (/)
74 df-2o 
 |-  2o = suc 1o
75 73 74 eqeq12i 
 |-  ( 1o = 2o <-> suc (/) = suc 1o )
76 0elon 
 |-  (/) e. On
77 1on 
 |-  1o e. On
78 suc11 
 |-  ( ( (/) e. On /\ 1o e. On ) -> ( suc (/) = suc 1o <-> (/) = 1o ) )
79 76 77 78 mp2an 
 |-  ( suc (/) = suc 1o <-> (/) = 1o )
80 75 79 bitri 
 |-  ( 1o = 2o <-> (/) = 1o )
81 43 80 nemtbir 
 |-  -. 1o = 2o
82 eqtr2 
 |-  ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) -> 1o = 2o )
83 81 82 mto 
 |-  -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o )
84 2on 
 |-  2o e. On
85 84 elexi 
 |-  2o e. _V
86 85 prid2 
 |-  2o e. { 1o , 2o }
87 86 nosgnn0i 
 |-  (/) =/= 2o
88 87 neii 
 |-  -. (/) = 2o
89 eqtr2 
 |-  ( ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) -> (/) = 2o )
90 88 89 mto 
 |-  -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o )
91 72 83 90 3pm3.2i 
 |-  ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) )
92 fvex 
 |-  ( ( A |` X ) ` x ) e. _V
93 92 92 brtp 
 |-  ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) <-> ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) \/ ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) \/ ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) )
94 3oran 
 |-  ( ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) \/ ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) \/ ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) <-> -. ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) )
95 93 94 bitri 
 |-  ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) <-> -. ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) )
96 95 con2bii 
 |-  ( ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) <-> -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) )
97 91 96 mpbi 
 |-  -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x )
98 simpl2l 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A |` X ) = ( B |` X ) )
99 98 adantr 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A |` X ) = ( B |` X ) )
100 99 fveq1d 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( A |` X ) ` x ) = ( ( B |` X ) ` x ) )
101 100 breq2d 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) <-> ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) ) )
102 97 101 mtbii 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) )
103 fvres 
 |-  ( x e. X -> ( ( A |` X ) ` x ) = ( A ` x ) )
104 fvres 
 |-  ( x e. X -> ( ( B |` X ) ` x ) = ( B ` x ) )
105 103 104 breq12d 
 |-  ( x e. X -> ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) <-> ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
106 105 notbid 
 |-  ( x e. X -> ( -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) <-> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
107 102 106 syl5ibcom 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( x e. X -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
108 44 intnanr 
 |-  -. ( (/) = 1o /\ 1o = (/) )
109 44 intnanr 
 |-  -. ( (/) = 1o /\ 1o = 2o )
110 81 intnan 
 |-  -. ( (/) = (/) /\ 1o = 2o )
111 108 109 110 3pm3.2i 
 |-  ( -. ( (/) = 1o /\ 1o = (/) ) /\ -. ( (/) = 1o /\ 1o = 2o ) /\ -. ( (/) = (/) /\ 1o = 2o ) )
112 0ex 
 |-  (/) e. _V
113 112 41 brtp 
 |-  ( (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } 1o <-> ( ( (/) = 1o /\ 1o = (/) ) \/ ( (/) = 1o /\ 1o = 2o ) \/ ( (/) = (/) /\ 1o = 2o ) ) )
114 3oran 
 |-  ( ( ( (/) = 1o /\ 1o = (/) ) \/ ( (/) = 1o /\ 1o = 2o ) \/ ( (/) = (/) /\ 1o = 2o ) ) <-> -. ( -. ( (/) = 1o /\ 1o = (/) ) /\ -. ( (/) = 1o /\ 1o = 2o ) /\ -. ( (/) = (/) /\ 1o = 2o ) ) )
115 113 114 bitri 
 |-  ( (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } 1o <-> -. ( -. ( (/) = 1o /\ 1o = (/) ) /\ -. ( (/) = 1o /\ 1o = 2o ) /\ -. ( (/) = (/) /\ 1o = 2o ) ) )
116 115 con2bii 
 |-  ( ( -. ( (/) = 1o /\ 1o = (/) ) /\ -. ( (/) = 1o /\ 1o = 2o ) /\ -. ( (/) = (/) /\ 1o = 2o ) ) <-> -. (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } 1o )
117 111 116 mpbi 
 |-  -. (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } 1o
118 45 46 breq12d 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) <-> (/) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } 1o ) )
119 117 118 mtbiri 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) )
120 fveq2 
 |-  ( x = X -> ( A ` x ) = ( A ` X ) )
121 fveq2 
 |-  ( x = X -> ( B ` x ) = ( B ` X ) )
122 120 121 breq12d 
 |-  ( x = X -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) ) )
123 122 notbid 
 |-  ( x = X -> ( -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> -. ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) ) )
124 119 123 syl5ibrcom 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( x = X -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
125 107 124 jaod 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( x e. X \/ x = X ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
126 69 125 sylbid 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( x C_ X -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
127 67 126 mpd 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) )
128 127 expr 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
129 128 ralrimiva 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
130 40 129 mtand 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. ( B ` X ) = 1o )
131 nofv 
 |-  ( B e. No -> ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) )
132 32 131 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) )
133 3orrot 
 |-  ( ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) <-> ( ( B ` X ) = 1o \/ ( B ` X ) = 2o \/ ( B ` X ) = (/) ) )
134 3orrot 
 |-  ( ( ( B ` X ) = 1o \/ ( B ` X ) = 2o \/ ( B ` X ) = (/) ) <-> ( ( B ` X ) = 2o \/ ( B ` X ) = (/) \/ ( B ` X ) = 1o ) )
135 133 134 bitri 
 |-  ( ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) <-> ( ( B ` X ) = 2o \/ ( B ` X ) = (/) \/ ( B ` X ) = 1o ) )
136 132 135 sylib 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( B ` X ) = 2o \/ ( B ` X ) = (/) \/ ( B ` X ) = 1o ) )
137 31 130 136 ecase23d 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( B ` X ) = 2o )