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 syl6ib
 |-  ( ( ( ( ( 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 )