Metamath Proof Explorer

Theorem nogt01o

Description: Given A greater than B , equal to B up to X , and B ( X ) undefined, then A ( X ) = 1o . (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 sltso 
 |-
2 simp11 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A e. No )
3 sonr 
 |-  ( (  -. A
4 1 2 3 sylancr 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. A
5 simpl2r 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A
6 simpl2l 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A |` X ) = ( B |` X ) )
7 simpl11 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A e. No )
8 nofun 
 |-  ( A e. No -> Fun A )
9 funrel 
 |-  ( Fun A -> Rel A )
10 8 9 syl 
 |-  ( A e. No -> Rel A )
11 7 10 syl 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  Rel A )
12 simpl13 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  X e. On )
13 simpr 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A ` X ) = (/) )
14 nolt02olem 
 |-  ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> dom A C_ X )
15 7 12 13 14 syl3anc 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  dom A C_ X )
16 relssres 
 |-  ( ( Rel A /\ dom A C_ X ) -> ( A |` X ) = A )
17 11 15 16 syl2anc 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A |` X ) = A )
18 simpl12 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  B e. No )
19 nofun 
 |-  ( B e. No -> Fun B )
20 funrel 
 |-  ( Fun B -> Rel B )
21 19 20 syl 
 |-  ( B e. No -> Rel B )
22 18 21 syl 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  Rel B )
23 simpl3 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( B ` X ) = (/) )
24 nolt02olem 
 |-  ( ( B e. No /\ X e. On /\ ( B ` X ) = (/) ) -> dom B C_ X )
25 18 12 23 24 syl3anc 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  dom B C_ X )
26 relssres 
 |-  ( ( Rel B /\ dom B C_ X ) -> ( B |` X ) = B )
27 22 25 26 syl2anc 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( B |` X ) = B )
28 6 17 27 3eqtr3d 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A = B )
29 5 28 breqtrrd 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A
30 4 29 mtand 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. ( A ` X ) = (/) )
31 simp2r 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  A
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 2 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 31 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 ralinexa 
 |-  ( A. 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 ) ) )
37 36 con2bii 
 |-  ( 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 ) ) )
38 35 37 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 ) ) )
39 1n0 
 |-  1o =/= (/)
40 39 neii 
 |-  -. 1o = (/)
41 eqtr2 
 |-  ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) -> 1o = (/) )
42 40 41 mto 
 |-  -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) )
43 df-2o 
 |-  2o = suc 1o
44 2on 
 |-  2o e. On
45 43 44 eqeltrri 
 |-  suc 1o e. On
46 45 onordi 
 |-  Ord suc 1o
47 1oex 
 |-  1o e. _V
48 47 sucid 
 |-  1o e. suc 1o
49 nordeq 
 |-  ( ( Ord suc 1o /\ 1o e. suc 1o ) -> suc 1o =/= 1o )
50 46 48 49 mp2an 
 |-  suc 1o =/= 1o
51 43 50 eqnetri 
 |-  2o =/= 1o
52 51 nesymi 
 |-  -. 1o = 2o
53 eqtr2 
 |-  ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) -> 1o = 2o )
54 52 53 mto 
 |-  -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o )
55 2on0 
 |-  2o =/= (/)
56 55 nesymi 
 |-  -. (/) = 2o
57 eqtr2 
 |-  ( ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) -> (/) = 2o )
58 56 57 mto 
 |-  -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o )
59 42 54 58 3pm3.2i 
 |-  ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) )
60 fvex 
 |-  ( ( A |` X ) ` x ) e. _V
61 60 60 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 ) ) )
62 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 ) ) )
63 61 62 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 ) ) )
64 63 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 ) )
65 59 64 mpbi 
 |-  -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x )
66 simpl2l 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A |` X ) = ( B |` X ) )
67 66 adantr 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A |` X ) = ( B |` X ) )
68 67 fveq1d 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( A |` X ) ` x ) = ( ( B |` X ) ` x ) )
69 68 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 ) ) )
70 65 69 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 ) )
71 fvres 
 |-  ( x e. X -> ( ( A |` X ) ` x ) = ( A ` x ) )
72 fvres 
 |-  ( x e. X -> ( ( B |` X ) ` x ) = ( B ` x ) )
73 71 72 breq12d 
 |-  ( x e. X -> ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) <-> ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
74 73 notbid 
 |-  ( x e. X -> ( -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) <-> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
75 70 74 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 ) ) )
76 51 neii 
 |-  -. 2o = 1o
77 76 intnanr 
 |-  -. ( 2o = 1o /\ (/) = (/) )
78 56 intnan 
 |-  -. ( 2o = 1o /\ (/) = 2o )
79 56 intnan 
 |-  -. ( 2o = (/) /\ (/) = 2o )
80 77 78 79 3pm3.2i 
 |-  ( -. ( 2o = 1o /\ (/) = (/) ) /\ -. ( 2o = 1o /\ (/) = 2o ) /\ -. ( 2o = (/) /\ (/) = 2o ) )
81 2oex 
 |-  2o e. _V
82 0ex 
 |-  (/) e. _V
83 81 82 brtp 
 |-  ( 2o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) <-> ( ( 2o = 1o /\ (/) = (/) ) \/ ( 2o = 1o /\ (/) = 2o ) \/ ( 2o = (/) /\ (/) = 2o ) ) )
84 3oran 
 |-  ( ( ( 2o = 1o /\ (/) = (/) ) \/ ( 2o = 1o /\ (/) = 2o ) \/ ( 2o = (/) /\ (/) = 2o ) ) <-> -. ( -. ( 2o = 1o /\ (/) = (/) ) /\ -. ( 2o = 1o /\ (/) = 2o ) /\ -. ( 2o = (/) /\ (/) = 2o ) ) )
85 83 84 bitri 
 |-  ( 2o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) <-> -. ( -. ( 2o = 1o /\ (/) = (/) ) /\ -. ( 2o = 1o /\ (/) = 2o ) /\ -. ( 2o = (/) /\ (/) = 2o ) ) )
86 85 con2bii 
 |-  ( ( -. ( 2o = 1o /\ (/) = (/) ) /\ -. ( 2o = 1o /\ (/) = 2o ) /\ -. ( 2o = (/) /\ (/) = 2o ) ) <-> -. 2o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) )
87 80 86 mpbi 
 |-  -. 2o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/)
88 simplr 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A ` X ) = 2o )
89 simpll3 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( B ` X ) = (/) )
90 88 89 breq12d 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) <-> 2o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) ) )
91 87 90 mtbiri 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) )
92 fveq2 
 |-  ( x = X -> ( A ` x ) = ( A ` X ) )
93 fveq2 
 |-  ( x = X -> ( B ` x ) = ( B ` X ) )
94 92 93 breq12d 
 |-  ( x = X -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) ) )
95 94 notbid 
 |-  ( x = X -> ( -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> -. ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) ) )
96 91 95 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 ) ) )
97 fveq2 
 |-  ( y = X -> ( A ` y ) = ( A ` X ) )
98 fveq2 
 |-  ( y = X -> ( B ` y ) = ( B ` X ) )
99 97 98 eqeq12d 
 |-  ( y = X -> ( ( A ` y ) = ( B ` y ) <-> ( A ` X ) = ( B ` X ) ) )
100 99 rspccv 
 |-  ( A. y e. x ( A ` y ) = ( B ` y ) -> ( X e. x -> ( A ` X ) = ( B ` X ) ) )
101 100 ad2antll 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( X e. x -> ( A ` X ) = ( B ` X ) ) )
102 eqcom 
 |-  ( ( A ` X ) = ( B ` X ) <-> ( B ` X ) = ( A ` X ) )
103 101 102 imbitrdi 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( X e. x -> ( B ` X ) = ( A ` X ) ) )
104 89 88 eqeq12d 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( B ` X ) = ( A ` X ) <-> (/) = 2o ) )
105 103 104 sylibd 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( X e. x -> (/) = 2o ) )
106 56 105 mtoi 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. X e. x )
107 simprl 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  x e. On )
108 simpl13 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  X e. On )
109 108 adantr 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  X e. On )
110 ontri1 
 |-  ( ( x e. On /\ X e. On ) -> ( x C_ X <-> -. X e. x ) )
111 onsseleq 
 |-  ( ( x e. On /\ X e. On ) -> ( x C_ X <-> ( x e. X \/ x = X ) ) )
112 110 111 bitr3d 
 |-  ( ( x e. On /\ X e. On ) -> ( -. X e. x <-> ( x e. X \/ x = X ) ) )
113 107 109 112 syl2anc 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( -. X e. x <-> ( x e. X \/ x = X ) ) )
114 106 113 mpbid 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( x e. X \/ x = X ) )
115 75 96 114 mpjaod 
 |-  ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) )
116 115 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 ) ) )
117 116 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 ) ) )
118 38 117 mtand 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  -. ( A ` X ) = 2o )
119 nofv 
 |-  ( A e. No -> ( ( A ` X ) = (/) \/ ( A ` X ) = 1o \/ ( A ` X ) = 2o ) )
120 2 119 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( A ` X ) = (/) \/ ( A ` X ) = 1o \/ ( A ` X ) = 2o ) )
121 3orcoma 
 |-  ( ( ( A ` X ) = (/) \/ ( A ` X ) = 1o \/ ( A ` X ) = 2o ) <-> ( ( A ` X ) = 1o \/ ( A ` X ) = (/) \/ ( A ` X ) = 2o ) )
122 120 121 sylib 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( ( A ` X ) = 1o \/ ( A ` X ) = (/) \/ ( A ` X ) = 2o ) )
123 30 118 122 ecase23d 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A  ( A ` X ) = 1o )